Clean up Equal.thy + some other tweaks

1 files changed, 5 insertions, 2 deletions

diff --git a/HoTT.thy b/HoTT.thy
index 3f2d475..e2a7e35 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -6,7 +6,6 @@ Homotopy type theory
 
 theory HoTT
 imports
-
 (* Basic theories *)
 HoTT_Base
 HoTT_Methods
@@ -22,18 +21,22 @@ Unit
 
 (* Derived definitions and properties *)
 EqualProps
-ProdProps
 Proj
 
 begin
 
+
 lemmas forms =
   Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
+
 lemmas intros =
   Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro
+
 lemmas elims =
   Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim
+
 lemmas routines =
   Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine
 
+
 end