From 49c008ef405ab8d8229ae1d5b0737339ee46e576 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 16:00:56 +0200
Subject: Clean up Equal.thy + some other tweaks

---
 HoTT.thy | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'HoTT.thy')

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
-- 
cgit v1.2.3