From 1be12499f63119d9455e2baa917659806732ca7d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 12 Jul 2018 01:46:30 +0200
Subject: Unit and Null types. Methods.

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

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 703f1aa..8c45d35 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -54,7 +54,7 @@ and
   Numeral_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n"
 
 lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans
-  \<comment> \<open>Lets \<open>standard\<close> automatically solve inequalities.\<close>
+  \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close>
 
 text "Universe types:"
 
@@ -64,6 +64,7 @@ where
   Universe_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)"
 and
   Universe_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)"
+  \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close>
 
 
 section \<open>Type families\<close>
-- 
cgit v1.2.3