Move Empty and Unit types to their own theories

1 files changed, 0 insertions, 13 deletions

diff --git a/Sum.thy b/Sum.thy
index f97bef1..8d0b0e6 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -66,17 +66,4 @@ lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2
 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim
 
 
-section \<open>Empty type\<close>
-
-axiomatization
-  Empty :: Term  ("\<zero>") and
-  indEmpty :: "Term \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
-where
-  Empty_form: "\<zero> : U(O)"
-and
-  Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
-
-lemmas Empty_routine [intro] = Empty_form Empty_elim
-
-
 end