From e6473c383b479610cee4c0119e5811a12a938cf9 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 14 Aug 2018 17:43:03 +0200
Subject: Well-formation rules are back in the methods; new theory synthesizing
 the natural number predecessor function.

---
 HoTT_Base.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'HoTT_Base.thy')

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
-- 
cgit v1.2.3