src/HOL/Induct/Mutil.ML

 qed "sing_Times_lemma";
 
 Goal "{i} Times below(n+n) : tiling domino";
 by (induct_tac "n" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
-by (resolve_tac tiling.intrs 1);
+by (rtac tiling.Un 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [sing_Times_lemma, domino.horiz])));
 qed "dominoes_tile_row";
 
 AddSIs [dominoes_tile_row]; 

 qed "domino_singleton_01";
 
 (*** Tilings of dominoes ***)
 
 Goal "t:tiling domino ==> finite t";
-by (eresolve_tac [tiling.induct] 1);
+by (etac tiling.induct 1);
 by Auto_tac;
 qed "tiling_domino_finite";
 
 Addsimps [tiling_domino_finite];
 
 Goal "t: tiling domino ==> card(colored 0 t) = card(colored 1 t)";
-by (eresolve_tac [tiling.induct] 1);
+by (etac tiling.induct 1);
 by (dtac domino_singleton_01 2);
 by Auto_tac;
 (*this lemma tells us that both "inserts" are non-trivial*)
 by (subgoal_tac "ALL p b. p : colored b a --> p ~: colored b t" 1);
 by (Asm_simp_tac 1);