diff options
| author | Josh Chen | 2018-08-14 17:43:03 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-14 17:43:03 +0200 |
| commit | e6473c383b479610cee4c0119e5811a12a938cf9 (patch) | |
| tree | 477ecc678909b6e29e064ede72b9dee0933c58ad /HoTT_Base.thy | |
| parent | f83534561085c224ab30343b945ee74d1ce547f4 (diff) | |
Well-formation rules are back in the methods; new theory synthesizing the natural number predecessor function.
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Base.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index e94ca5c..4fadd5d 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -78,7 +78,7 @@ section \<open>Named theorems\<close> text " Named theorems to be used by proof methods later (see HoTT_Methods.thy). - \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are used by the simplification method as equational rewrite rules. + \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting. " named_theorems wellform |