src/HOL/UNITY/Comp.ML

      "[| strict_ex_prop X;  States F = States G |] \
 \     ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = \
 \         (F:X --> G:X)";
 by Safe_tac;
 by (Blast_tac 1);
-auto();
+by Auto_tac;
 qed "strict_ex_refine_lemma";
 
 Goalw [strict_ex_prop_def]
      "[| strict_ex_prop X;  States F = States G |] \
 \     ==> (ALL H. States F = States H & F Join H : welldef & F Join H : X \

 
 Goal "[| strict_ex_prop X;  States F = States G;  \
 \        ALL H. States F = States H & F Join H : welldef Int X \
 \          --> G Join H : welldef |] \
 \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
-bd sym 1;
+by (dtac sym 1);
 by (res_inst_tac [("x","SKIP (States G)")] allE 1
     THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
 					   strict_ex_refine_lemma_v]) 1);
 qed "ex_refinement_thm";