diff options
author | Josh Chen | 2018-09-16 11:03:48 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-16 11:03:48 +0200 |
commit | d4900ced2e071927d81a21a9127034941f258ec3 (patch) | |
tree | c0289b3fd8337a05baa7740ca3f5e84c57f539ca /HoTT_Methods.thy | |
parent | 515872533295e8464799467303fff923b52a2c01 (diff) | |
parent | f0999d07a0f41284ba84fae725a0186e0ec9ff5f (diff) |
Reorganized HoTT_Base, updated theories
Diffstat (limited to 'HoTT_Methods.thy')
-rw-r--r-- | HoTT_Methods.thy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 32e412b..abb6dda 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -14,12 +14,12 @@ begin section \<open>Deriving typing judgments\<close> +method routine uses lems = (assumption | rule lems | standard)+ + text " - \<open>routine\<close> proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. + @{method routine} proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. " -method routine uses lems = (assumption | rule lems | standard)+ - text " \<open>wellformed'\<close> finds a proof of any valid typing judgment derivable from the judgment passed as \<open>jdmt\<close>. If no judgment is passed, it will try to resolve with the theorems declared \<open>wellform\<close>. |