diff options
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>. |