From decb363a30a30c1875bf4b93bc544c28edf3149e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 7 Jul 2018 23:03:33 +0200
Subject: Library snapshot. Methods written, everything nicely organized.

---
 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 cfced79..60e5167 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -15,7 +15,7 @@ section \<open>Setup\<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 used when simplifying function application."
+\<open>comp\<close> declares computation rules, which are used by the simplification method as equational rewrite rules."
 
 named_theorems wellform
 named_theorems comp
-- 
cgit v1.2.3