diff -r ed18feb34c07 -r fae6051ec192 src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Sun Apr 09 19:03:55 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(*  Title:      CTT/Bool.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-*)
-
-section \<open>The two-element type (booleans and conditionals)\<close>
-
-theory Bool
-  imports CTT
-begin
-
-definition Bool :: "t"
-  where "Bool \<equiv> T+T"
-
-definition true :: "i"
-  where "true \<equiv> inl(tt)"
-
-definition false :: "i"
-  where "false \<equiv> inr(tt)"
-
-definition cond :: "[i,i,i]\<Rightarrow>i"
-  where "cond(a,b,c) \<equiv> when(a, \<lambda>_. b, \<lambda>_. c)"
-
-lemmas bool_defs = Bool_def true_def false_def cond_def
-
-
-subsection \<open>Derivation of rules for the type \<open>Bool\<close>\<close>
-
-text \<open>Formation rule.\<close>
-lemma boolF: "Bool type"
-  unfolding bool_defs by typechk
-
-text \<open>Introduction rules for \<open>true\<close>, \<open>false\<close>.\<close>
-
-lemma boolI_true: "true : Bool"
-  unfolding bool_defs by typechk
-
-lemma boolI_false: "false : Bool"
-  unfolding bool_defs by typechk
-
-text \<open>Elimination rule: typing of \<open>cond\<close>.\<close>
-lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
-  unfolding bool_defs
-  apply (typechk; erule TE)
-   apply typechk
-  done
-
-lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
-  \<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
-  unfolding bool_defs
-  apply (rule PlusEL)
-    apply (erule asm_rl refl_elem [THEN TEL])+
-  done
-
-text \<open>Computation rules for \<open>true\<close>, \<open>false\<close>.\<close>
-
-lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
-  unfolding bool_defs
-  apply (rule comp_rls)
-    apply typechk
-   apply (erule_tac [!] TE)
-   apply typechk
-  done
-
-lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
-  unfolding bool_defs
-  apply (rule comp_rls)
-    apply typechk
-   apply (erule_tac [!] TE)
-   apply typechk
-  done
-
-end