1 files changed, 11 insertions, 7 deletions

diff --git a/HoTT.thy b/HoTT.thy
index abb1085..0e7a674 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -1,12 +1,13 @@
-(*  Title:  HoTT/HoTT.thy
-    Author: Josh Chen
+(*
+Title:  HoTT.thy
+Author: Joshua Chen
+Date:   2018
 
 Homotopy type theory
 *)
 
 theory HoTT
 imports
-
 (* Basic theories *)
 HoTT_Base
 HoTT_Methods
@@ -22,18 +23,21 @@ 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
+
+text \<open>Rule bundles:\<close>
+
 lemmas intros =
-  Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro
+  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