diff options
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 99f3446..088c1fa 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -9,6 +9,7 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" begin + section \<open>Substitution and simplification\<close> ML_file "~~/src/Tools/misc_legacy.ML" @@ -25,6 +26,7 @@ Premises of the rule(s) applied are added as new subgoals. method compute declares comp = (subst comp) + section \<open>Handling universes\<close> text \<open> @@ -46,6 +48,7 @@ method cumulativity declares form = ( ((elim U_cumulative | (rule U_cumulative, rule form)), provelt) ) + section \<open>Deriving typing judgments\<close> method routine uses add = (assumption | rule add | rule)+ @@ -54,6 +57,7 @@ text \<open> The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}. \<close> + section \<open>Derivation search\<close> text \<open> @@ -63,6 +67,7 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}. method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ + section \<open>Induction\<close> text \<open> |