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 9849195..411176e 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -50,10 +50,10 @@ method derive uses lems = (routine add: lems | compute comp: lems)+ section \<open>Induction\<close> -text " +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>. -" +\<close> end |