From 38dd685f6929d402a32ddfe2d913c7b380b9e935 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 3 Mar 2019 22:47:03 +0100
Subject: Improve automated handling of universes. derive now can automatically
 handle more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop
 as much.

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

(limited to 'HoTT_Methods.thy')

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>
 
-- 
cgit v1.2.3

