From 7823d59b2d9436f1bf0042fff62ee2bcc4c29ec0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 3 Jul 2018 18:57:57 +0200
Subject: Refactor HoTT_Methods.thy, proved more stuff with new methods.

---
 HoTT.thy | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

(limited to 'HoTT.thy')

diff --git a/HoTT.thy b/HoTT.thy
index b500150..42796c1 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -7,10 +7,19 @@ Load all the component modules for the HoTT logic.
 theory HoTT
 
 imports
-  HoTT_Base
-  HoTT_Methods
-  Prod
-  Sum
+
+(* Basic theories *)
+HoTT_Base
+HoTT_Methods
+
+(* Types *)
+Equal
+Prod
+Sum
+
+(* Additional properties *)
+EqualProps
+Proj
 
 begin
 end
-- 
cgit v1.2.3