Library organization and formatting

4 files changed, 10 insertions, 9 deletions

diff --git a/Equal.thy b/Equal.thy
index 12ed272..02fe540 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -7,7 +7,6 @@ Equality type.
 
 theory Equal
   imports HoTT_Base
-
 begin
 
 axiomatization
diff --git a/HoTT.thy b/HoTT.thy
index 405364e..b500150 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -4,12 +4,13 @@
 Load all the component modules for the HoTT logic.
 *)
 
-theory HoTT imports
+theory HoTT
+
+imports
   HoTT_Base
-  Prod Sum
+  HoTT_Methods
+  Prod
+  Sum
 
 begin
-
-\<comment> \<open>Maybe tactic setup can go in here?\<close>
-
-end
\ No newline at end of file
+end
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index a0078fa..561dbe6 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -17,7 +17,7 @@ text "Set up type checking routines, proof methods etc."
 section \<open>Metalogical definitions\<close>
 
 text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
-We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ``\<open>a\<close> is a type''."
+We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ''\<open>a\<close> is a type''."
 
 typedecl Term
 
@@ -32,6 +32,8 @@ consts
   is_a_type :: "Term \<Rightarrow> prop"           ("(1_ :/ U)" [0] 1000)
   is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
 
+text "The following fact is used to make explicit the assumption of well-formed contexts."
+
 axiomatization where
   inhabited_implies_type [intro, elim]: "\<And>a A. a : A \<Longrightarrow> A : U"
 
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index 871c553..a3a1f63 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -1,6 +1,5 @@
 theory HoTT_Theorems
   imports HoTT
-
 begin
 
 text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.