aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Methods.thy
diff options
context:
space:
mode:
Diffstat (limited to 'HoTT_Methods.thy')
-rw-r--r--HoTT_Methods.thy5
1 files changed, 3 insertions, 2 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 27f252b..e45608e 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -64,11 +64,12 @@ section \<open>Derivation search\<close>
text \<open>
The method @{theory_text derive} combines @{method routine} and @{method compute} to search for derivations of judgments.
-It also handles universes using @{method hierarchy} and @{method cumulativity}.
+It also handles universes using @{method cumulativity}.
+The method @{method hierarchy} has been observed to cause looping in previous versions, and is hence no longer part of @{theory_text derive}.
\<close>
method derive uses lems declares comp =
- (routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+
+ (routine add: lems | compute add: lems comp: comp | cumulativity form: lems)+
section \<open>Additional method combinators\<close>