aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Methods.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--HoTT_Methods.thy1
1 files changed, 0 insertions, 1 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index ad7384d..27f252b 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -70,7 +70,6 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}.
method derive uses lems declares comp =
(routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+
-
section \<open>Additional method combinators\<close>
text \<open>