From 07d312b312c3058551353bcf403a1dc7c7c83311 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 31 Jan 2019 15:51:24 +0100
Subject: Text remarks

---
 HoTT_Base.thy | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 99ab5ce..bb47a74 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -2,7 +2,7 @@
 Isabelle/HoTT: Foundational definitions and notation
 Jan 2019
 
-This file is the starting point, and contains the base setup and definitions of the object logic.
+This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
 Among other things, it defines:
 
 * Meta-numerals to index the universe hierarchy, and related axioms.
@@ -18,7 +18,7 @@ begin
 
 section \<open>Basic setup\<close>
 
-declare[[eta_contract=false]] (* I'm not actually sure this does anything... *)
+declare[[eta_contract=false]] (* Does this option actually do anything? *)
 
 typedecl t  \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 typedecl ord  \<comment> \<open>Type of meta-numerals\<close>
@@ -55,9 +55,13 @@ text \<open>
 Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination.
 Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 
-@{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}.
+@{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}.
 \<close>
 
+section \<open>Type families\<close>
+
+abbrev (input) 
+
 section \<open>Named theorems\<close>
 
 named_theorems comp
-- 
cgit v1.2.3