diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Bool.ML
--- a/src/ZF/Bool.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Bool.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -24,6 +24,8 @@
 by (rtac consI1 1);
 qed "bool_0I";
 
+Addsimps [bool_1I, bool_0I];
+
 Goalw bool_defs "1~=0";
 by (rtac succ_not_0 1);
 qed "one_not_0";
@@ -54,10 +56,16 @@
 fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
 
 
-Goal "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
+Goal "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
 by (bool_tac 1);
 qed "cond_type";
 
+(*For Simp_tac and Blast_tac*)
+Goal "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A";
+by (bool_tac 1);
+qed "cond_simple_type";
+Addsimps [cond_simple_type];
+
 val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
 by (rewtac rew);
 by (rtac cond_1 1);
@@ -89,10 +97,14 @@
     "[| a:bool;  b:bool |] ==> a or b : bool"
  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
 
+Addsimps [not_type, and_type, or_type];
+
 qed_goalw "xor_type" Bool.thy [xor_def]
     "[| a:bool;  b:bool |] ==> a xor b : bool"
  (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
 
+Addsimps [xor_type];
+
 val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
                        or_type, xor_type];