From e1be5f97bb2a42b3179bc24b118d69af137f8e5d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 21:28:21 +0200
Subject: Regrouping type rules

---
 HoTT_Methods.thy | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 316841d..4d2174b 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -1,6 +1,5 @@
 (*  Title:  HoTT/HoTT_Methods.thy
     Author: Josh Chen
-    Date:   Jun 2018
 
 Method setup for the HoTT library. Relies heavily on Eisbach.
 *)
@@ -18,7 +17,7 @@ section \<open>Method definitions\<close>
 subsection \<open>Simple type rule proof search\<close>
 
 text "
-  Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] and [elim] (in the respective theory files), as well as additional provided lemmas.
+  Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] in the respective theory files, as well as additional provided lemmas.
   
   Can also perform typechecking, and search for elements of a type.
 "
@@ -62,7 +61,7 @@ ML_file "~~/src/Tools/eqsubst.ML"
 
 text "Perform basic single-step computations:"
 
-method compute uses lems = (subst lems comp)
+method compute uses lems = (subst lems comp | rule lems comp)
 
 
 end
-- 
cgit v1.2.3