diff options
| author | Josh Chen | 2019-02-22 23:45:50 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-22 23:45:50 +0100 |
| commit | 57d183c7955fb54b3eb6dd431f5aec338131266b (patch) | |
| tree | ae6bfabbd8fcd63ee7d5140ca842599efbd58c16 /HoTT_Methods.thy | |
| parent | 0036345412d5c145b63693ed672b175018fa3791 (diff) | |
Cleanups and reorganization
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Methods.thy | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 099a73e..c9744e9 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -51,7 +51,7 @@ method cumulativity declares form = ( section \<open>Deriving typing judgments\<close> -method routine uses add = (rule add | assumption | rule)+ +method routine uses add = (assumption | rule add | rule)+ 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}. @@ -65,7 +65,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute It also handles universes using @{method hierarchy} and @{method cumulativity}. \<close> -method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ +method derive uses lems = + (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ section \<open>Additional method combinators\<close> |