diff options
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Methods.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 8351c3c..f80b99b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -57,9 +57,9 @@ method derive uses lems unfolds = ( unfold unfolds | simple lems: lems | match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> | - rule U_hierarchy | + rule U_hierarchy (*| (rule U_cumulative, simple lems: lems) | - (rule U_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>) + (rule U_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>)*) )+ |