src/HOL/UNITY/PPROD.ML

 
 (** lift_act and drop_act **)
 
 Goalw [lift_act_def] "lift_act i Id = Id";
 by Auto_tac;
-be rev_mp 1;
-bd sym 1;
+by (etac rev_mp 1);
+by (dtac sym 1);
 by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
 qed "lift_act_Id";
 Addsimps [lift_act_Id];
 
 Goalw [drop_act_def] "(s, s') : act ==> (s i, s' i) : drop_act i act";

 by Auto_tac;
 by (res_inst_tac [("x", "f(i:=a)")] exI 1);
 by (Asm_simp_tac 1);
 by (res_inst_tac [("x", "f(i:=b)")] exI 1);
 by (Asm_simp_tac 1);
-br ext 1;
+by (rtac ext 1);
 by (Asm_simp_tac 1);
 qed "lift_act_inverse";
 Addsimps [lift_act_inverse];
 
 Goal "inj (lift_act i)";

 
 (*For compatibility with the original definition and perhaps simpler proofs*)
 Goalw [lift_act_def]
     "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
 by Auto_tac;
-br exI 1;
+by (rtac exI 1);
 by Auto_tac;
 qed "lift_act_eq";
 AddIffs [lift_act_eq];
 
 

      simpset() addsimps [Acts_PLam]));
 qed "reachable_PLam";
 
 (*Result to justify a re-organization of this file*)
 Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
-auto();
+by Auto_tac;
 result();
 
 Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
 by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
 qed "reachable_PLam_subset1";