Refactor HoTT_Methods.thy, proved more stuff with new methods.

1 files changed, 13 insertions, 4 deletions

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