aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy
diff options
context:
space:
mode:
authorJosh Chen2018-09-17 13:13:55 +0200
committerJosh Chen2018-09-17 13:13:55 +0200
commit76ac8ed82317f3f62f26ecc88f412c61004bcffa (patch)
tree02f3f3f5f87027d38520e376c577e7e6621fa6cf /HoTT.thy
parentea0c0c5427888982adce10ab25cebe445997f08b (diff)
Reorganizing theories
Diffstat (limited to '')
-rw-r--r--HoTT.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT.thy b/HoTT.thy
index abb1085..3f2d475 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -30,7 +30,7 @@ begin
lemmas forms =
Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
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 =