diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/Bool.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -8,20 +8,80 @@
 
 theory Bool
 imports CTT
-uses "~~/src/Provers/typedsimp.ML" "rew.ML"
 begin
 
-consts
-  Bool        :: "t"
-  true        :: "i"
-  false       :: "i"
-  cond        :: "[i,i,i]=>i"
-defs
-  Bool_def:   "Bool == T+T"
-  true_def:   "true == inl(tt)"
-  false_def:  "false == inr(tt)"
-  cond_def:   "cond(a,b,c) == when(a, %u. b, %u. c)"
+constdefs
+  Bool :: "t"
+  "Bool == T+T"
+
+  true :: "i"
+  "true == inl(tt)"
+
+  false :: "i"
+  "false == inr(tt)"
+
+  cond :: "[i,i,i]=>i"
+  "cond(a,b,c) == when(a, %u. b, %u. c)"
+
+lemmas bool_defs = Bool_def true_def false_def cond_def
+
+
+subsection {* Derivation of rules for the type Bool *}
+
+(*formation rule*)
+lemma boolF: "Bool type"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
+
+
+(*introduction rules for true, false*)
+
+lemma boolI_true: "true : Bool"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolI_false: "false : Bool"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
 
-ML {* use_legacy_bindings (the_context ()) *}
+(*elimination rule: typing of cond*)
+lemma boolE: 
+    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolEL: 
+    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
+     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
+apply (unfold bool_defs)
+apply (rule PlusEL)
+apply (erule asm_rl refl_elem [THEN TEL])+
+done
+
+(*computation rules for true, false*)
+
+lemma boolC_true: 
+    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
+apply (unfold bool_defs)
+apply (rule comp_rls)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolC_false: 
+    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
+apply (unfold bool_defs)
+apply (rule comp_rls)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
 
 end