src/ZF/Bool.ML

 (** 1=0 ==> R **)
 val one_neq_0 = one_not_0 RS notE;
 
 val major::prems = goalw Bool.thy bool_defs
     "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
-br (major RS consE) 1;
+by (rtac (major RS consE) 1);
 by (REPEAT (eresolve_tac (singletonE::prems) 1));
 val boolE = result();
 
 (** cond **)
 

 goal Bool.thy "!!a. a: bool ==> a and a = a";
 by (bool0_tac 1);
 val and_absorb = result();
 
 goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
-be boolE 1;
+by (etac boolE 1);
 by (bool0_tac 1);
 by (bool0_tac 1);
 val and_commute = result();
 
 goal Bool.thy

 goal Bool.thy "!!a. a: bool ==> a or a = a";
 by (bool0_tac 1);
 val or_absorb = result();
 
 goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
-be boolE 1;
+by (etac boolE 1);
 by (bool0_tac 1);
 by (bool0_tac 1);
 val or_commute = result();
 
 goal Bool.thy "!!a. a: bool ==> (a or b) or c  =  a or (b or c)";