Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!

1 files changed, 1 insertions, 0 deletions

diff --git a/Nat.thy b/Nat.thy
index 46b1af5..8a55852 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -41,6 +41,7 @@ where
     C: \<nat> \<longrightarrow> U i;
     \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
+lemmas Nat_form [form]
 lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
 lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ