diff options
| author | Josh Chen | 2019-02-11 15:37:18 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-11 15:37:18 +0100 |
| commit | a5692e0ba36b372b9175d7b356f4b2fd1ee3d663 (patch) | |
| tree | fbd980759d3442c21f3859cd07669b1f6db59c71 /HoTT_Methods.thy | |
| parent | da8edcc1162044c33053ea64c4efbd4910b6cec7 (diff) | |
Put typing functionality into a .thy and clean up antiquotations, which results in some reorganization of the theory import structure.
Diffstat (limited to '')
| -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> |