From dcf87145a1059659099bbecde55973de0d36d43f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 03:04:37 +0200
Subject: Theories fully reorganized. Well-formedness rules removed. New
 methods etc.

---
 HoTT_Methods.thy | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 411176e..8929f69 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -3,14 +3,11 @@ Title:  HoTT_Methods.thy
 Author: Joshua Chen
 Date:   2018
 
-Method setup for the HoTT logic. Relies heavily on Eisbach.
+Method setup for the HoTT logic.
 *)
 
 theory HoTT_Methods
-imports
-  "HOL-Eisbach.Eisbach"
-  "HOL-Eisbach.Eisbach_Tools"
-  HoTT_Base
+imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 
 begin
 
@@ -43,16 +40,19 @@ Premises of the rule(s) applied are added as new subgoals.
 
 section \<open>Derivation search\<close>
 
-text \<open>Combine @{method routine} and @{method compute} to search for derivations of judgments.\<close>
+text \<open>
+Combine @{method routine} and @{method compute} to search for derivations of judgments.
+Also handle universes using methods @{method hierarchy} and @{method cumulativity} defined in @{file HoTT_Base.thy}.
+\<close>
 
-method derive uses lems = (routine add: lems | compute comp: lems)+
+method derive uses lems = (routine add: lems | compute comp: lems | cumulativity | hierarchy)+
 
 
 section \<open>Induction\<close>
 
 text \<open>
-  Placeholder section for the automation of induction, i.e. using the elimination rules.
-  At the moment one must directly apply them with \<open>rule X_elim\<close>.
+Placeholder section for the automation of induction, i.e. using the elimination rules.
+At the moment one must directly apply them with \<open>rule X_elim\<close>.
 \<close>
 
 
-- 
cgit v1.2.3