merged
authorwenzelm
Thu Oct 30 23:14:11 2014 +0100 (2014-10-30)
changeset 58840f4bb3068d819
parent 58834 773b378d9313
parent 58839 ccda99401bc8
child 58841 e16712bb1d41
child 58842 22b87ab47d3b
merged
     1.1 --- a/src/FOL/ex/Miniscope.thy	Thu Oct 30 21:02:01 2014 +0100
     1.2 +++ b/src/FOL/ex/Miniscope.thy	Thu Oct 30 23:14:11 2014 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4  
     1.5  ML {*
     1.6  val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
     1.7 -fun mini_tac ctxt = rtac @{thm ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
     1.8 +fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
     1.9  *}
    1.10  
    1.11  end
     2.1 --- a/src/FOL/simpdata.ML	Thu Oct 30 21:02:01 2014 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Thu Oct 30 23:14:11 2014 +0100
     2.3 @@ -107,7 +107,9 @@
     2.4  val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
     2.5  
     2.6  fun unsafe_solver ctxt =
     2.7 -  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), atac, etac @{thm FalseE}];
     2.8 +  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt),
     2.9 +    assume_tac,
    2.10 +    eresolve_tac @{thms FalseE}];
    2.11  
    2.12  (*No premature instantiation of variables during simplification*)
    2.13  fun safe_solver ctxt =
     3.1 --- a/src/HOL/Fun.thy	Thu Oct 30 21:02:01 2014 +0100
     3.2 +++ b/src/HOL/Fun.thy	Thu Oct 30 23:14:11 2014 +0100
     3.3 @@ -839,8 +839,8 @@
     3.4        | (T, SOME rhs) =>
     3.5            SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
     3.6              (fn _ =>
     3.7 -              rtac eq_reflection 1 THEN
     3.8 -              rtac @{thm ext} 1 THEN
     3.9 +              resolve_tac [eq_reflection] 1 THEN
    3.10 +              resolve_tac @{thms ext} 1 THEN
    3.11                simp_tac (put_simpset ss ctxt) 1))
    3.12      end
    3.13  in proc end
     4.1 --- a/src/HOL/HOL.thy	Thu Oct 30 21:02:01 2014 +0100
     4.2 +++ b/src/HOL/HOL.thy	Thu Oct 30 23:14:11 2014 +0100
     4.3 @@ -905,7 +905,7 @@
     4.4  apply (rule ex1E [OF major])
     4.5  apply (rule prem)
     4.6  apply (tactic {* ares_tac @{thms allI} 1 *})+
     4.7 -apply (tactic {* etac (Classical.dup_elim @{thm allE}) 1 *})
     4.8 +apply (tactic {* eresolve_tac [Classical.dup_elim @{thm allE}] 1 *})
     4.9  apply iprover
    4.10  done
    4.11  
    4.12 @@ -1822,7 +1822,7 @@
    4.13  proof
    4.14    assume "PROP ?ofclass"
    4.15    show "PROP ?equal"
    4.16 -    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
    4.17 +    by (tactic {* ALLGOALS (resolve_tac [Thm.unconstrainT @{thm eq_equal}]) *})
    4.18        (fact `PROP ?ofclass`)
    4.19  next
    4.20    assume "PROP ?equal"
    4.21 @@ -1921,7 +1921,10 @@
    4.22    let
    4.23      fun eval_tac ctxt =
    4.24        let val conv = Code_Runtime.dynamic_holds_conv ctxt
    4.25 -      in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
    4.26 +      in
    4.27 +        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
    4.28 +        resolve_tac [TrueI]
    4.29 +      end
    4.30    in
    4.31      Scan.succeed (SIMPLE_METHOD' o eval_tac)
    4.32    end
    4.33 @@ -1932,7 +1935,7 @@
    4.34      SIMPLE_METHOD'
    4.35        (CHANGED_PROP o
    4.36          (CONVERSION (Nbe.dynamic_conv ctxt)
    4.37 -          THEN_ALL_NEW (TRY o rtac TrueI))))
    4.38 +          THEN_ALL_NEW (TRY o resolve_tac [TrueI]))))
    4.39  *} "solve goal by normalization"
    4.40  
    4.41  
    4.42 @@ -1979,7 +1982,7 @@
    4.43      val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
    4.44    in
    4.45      fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    4.46 -    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
    4.47 +    fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac];
    4.48    end;
    4.49  
    4.50    local
     5.1 --- a/src/HOL/Product_Type.thy	Thu Oct 30 21:02:01 2014 +0100
     5.2 +++ b/src/HOL/Product_Type.thy	Thu Oct 30 23:14:11 2014 +0100
     5.3 @@ -1324,9 +1324,10 @@
     5.4                        SOME (Goal.prove ctxt [] []
     5.5                          (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
     5.6                          (K (EVERY
     5.7 -                          [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
     5.8 -                           rtac subsetI 1, dtac CollectD 1, simp,
     5.9 -                           rtac subsetI 1, rtac CollectI 1, simp])))
    5.10 +                          [resolve_tac [eq_reflection] 1,
    5.11 +                           resolve_tac @{thms subset_antisym} 1,
    5.12 +                           resolve_tac [subsetI] 1, dresolve_tac [CollectD] 1, simp,
    5.13 +                           resolve_tac [subsetI] 1, resolve_tac [CollectI] 1, simp])))
    5.14                      end
    5.15                    else NONE)
    5.16            | _ => NONE)
     6.1 --- a/src/HOL/Set.thy	Thu Oct 30 21:02:01 2014 +0100
     6.2 +++ b/src/HOL/Set.thy	Thu Oct 30 23:14:11 2014 +0100
     6.3 @@ -71,10 +71,11 @@
     6.4  simproc_setup defined_Collect ("{x. P x & Q x}") = {*
     6.5    fn _ => Quantifier1.rearrange_Collect
     6.6      (fn _ =>
     6.7 -      rtac @{thm Collect_cong} 1 THEN
     6.8 -      rtac @{thm iffI} 1 THEN
     6.9 +      resolve_tac @{thms Collect_cong} 1 THEN
    6.10 +      resolve_tac @{thms iffI} 1 THEN
    6.11        ALLGOALS
    6.12 -        (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
    6.13 +        (EVERY' [REPEAT_DETERM o eresolve_tac @{thms conjE},
    6.14 +          DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
    6.15  *}
    6.16  
    6.17  lemmas CollectE = CollectD [elim_format]
    6.18 @@ -382,7 +383,7 @@
    6.19  
    6.20  setup {*
    6.21    map_theory_claset (fn ctxt =>
    6.22 -    ctxt addbefore ("bspec", fn _ => dtac @{thm bspec} THEN' assume_tac))
    6.23 +    ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac))
    6.24  *}
    6.25  
    6.26  ML {*
     7.1 --- a/src/HOL/Tools/Function/function_lib.ML	Thu Oct 30 21:02:01 2014 +0100
     7.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Thu Oct 30 23:14:11 2014 +0100
     7.3 @@ -113,7 +113,7 @@
     7.4              then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
     7.5              else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
     7.6       (K (rewrite_goals_tac ctxt ac
     7.7 -         THEN rtac Drule.reflexive_thm 1))
     7.8 +         THEN resolve_tac [Drule.reflexive_thm] 1))
     7.9   end
    7.10  
    7.11  (* instance for unions *)
     8.1 --- a/src/HOL/Tools/Function/partial_function.ML	Thu Oct 30 21:02:01 2014 +0100
     8.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Thu Oct 30 23:14:11 2014 +0100
     8.3 @@ -90,7 +90,7 @@
     8.4                if Term.is_open arg then no_tac
     8.5                else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
     8.6                  THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
     8.7 -                THEN_ALL_NEW etac @{thm thin_rl}
     8.8 +                THEN_ALL_NEW eresolve_tac @{thms thin_rl}
     8.9                  THEN_ALL_NEW (CONVERSION
    8.10                    (params_conv ~1 (fn ctxt' =>
    8.11                      arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
    8.12 @@ -290,7 +290,7 @@
    8.13      val rec_rule = let open Conv in
    8.14        Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
    8.15          CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
    8.16 -        THEN rtac @{thm refl} 1) end;
    8.17 +        THEN resolve_tac @{thms refl} 1) end;
    8.18    in
    8.19      lthy'
    8.20      |> Local_Theory.note (eq_abinding, [rec_rule])
     9.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Oct 30 21:02:01 2014 +0100
     9.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Oct 30 23:14:11 2014 +0100
     9.3 @@ -167,19 +167,19 @@
     9.4            (rename_bound_vars_RS th rl handle THM _ => tryall rls)
     9.5    in  tryall rls  end;
     9.6  
     9.7 -(* Special version of "rtac" that works around an explosion in the unifier.
     9.8 +(* Special version of "resolve_tac" that works around an explosion in the unifier.
     9.9     If the goal has the form "?P c", the danger is that resolving it against a
    9.10     property of the form "... c ... c ... c ..." will lead to a huge unification
    9.11     problem, due to the (spurious) choices between projection and imitation. The
    9.12     workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
    9.13 -fun quant_rtac th i st =
    9.14 +fun quant_resolve_tac th i st =
    9.15    case (concl_of st, prop_of th) of
    9.16      (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
    9.17      let
    9.18        val cc = cterm_of (theory_of_thm th) c
    9.19        val ct = Thm.dest_arg (cprop_of th)
    9.20 -    in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    9.21 -  | _ => rtac th i st
    9.22 +    in resolve_tac [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    9.23 +  | _ => resolve_tac [th] i st
    9.24  
    9.25  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    9.26    e.g. from conj_forward, should have the form
    9.27 @@ -187,7 +187,7 @@
    9.28    and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
    9.29  fun forward_res ctxt nf st =
    9.30    let
    9.31 -    fun tacf [prem] = quant_rtac (nf prem) 1
    9.32 +    fun tacf [prem] = quant_resolve_tac (nf prem) 1
    9.33        | tacf prems =
    9.34          error (cat_lines
    9.35            ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
    9.36 @@ -288,7 +288,7 @@
    9.37  fun forward_res2 nf hyps st =
    9.38    case Seq.pull
    9.39          (REPEAT
    9.40 -         (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    9.41 +         (Misc_Legacy.METAHYPS (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
    9.42           st)
    9.43    of SOME(th,_) => th
    9.44     | NONE => raise THM("forward_res2", 0, [st]);
    9.45 @@ -700,14 +700,14 @@
    9.46  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    9.47  
    9.48  fun skolemize_prems_tac ctxt prems =
    9.49 -  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE
    9.50 +  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac [exE]
    9.51  
    9.52  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
    9.53    Function mkcl converts theorems to clauses.*)
    9.54  fun MESON preskolem_tac mkcl cltac ctxt i st =
    9.55    SELECT_GOAL
    9.56      (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
    9.57 -            rtac @{thm ccontr} 1,
    9.58 +            resolve_tac @{thms ccontr} 1,
    9.59              preskolem_tac,
    9.60              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
    9.61                        EVERY1 [skolemize_prems_tac ctxt negs,
    10.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 30 21:02:01 2014 +0100
    10.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 30 23:14:11 2014 +0100
    10.3 @@ -208,8 +208,8 @@
    10.4        |> Drule.beta_conv cabs |> Thm.apply cTrueprop
    10.5      fun tacf [prem] =
    10.6        rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
    10.7 -      THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
    10.8 -                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
    10.9 +      THEN resolve_tac [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
   10.10 +                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1
   10.11    in
   10.12      Goal.prove_internal ctxt [ex_tm] conc tacf
   10.13      |> forall_intr_list frees
    11.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Oct 30 21:02:01 2014 +0100
    11.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Oct 30 23:14:11 2014 +0100
    11.3 @@ -531,7 +531,7 @@
    11.4      if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
    11.5    | copy_prems_tac (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
    11.6    | copy_prems_tac (m :: ms) ns i =
    11.7 -    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
    11.8 +    eresolve_tac [copy_prem] i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
    11.9  
   11.10  (* Metis generates variables of the form _nnn. *)
   11.11  val is_metis_fresh_variable = String.isPrefix "_"
   11.12 @@ -578,10 +578,10 @@
   11.13          end
   11.14        | _ => raise Fail "expected a single non-zapped, non-Metis Var")
   11.15    in
   11.16 -    (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
   11.17 +    (DETERM (eresolve_tac @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
   11.18    end
   11.19  
   11.20 -fun fix_exists_tac t = etac exE THEN' rename_tac [t |> dest_Var |> fst |> fst]
   11.21 +fun fix_exists_tac t = eresolve_tac [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
   11.22  
   11.23  fun release_quantifier_tac thy (skolem, t) =
   11.24    (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
   11.25 @@ -730,7 +730,8 @@
   11.26                         cat_lines (map string_of_subst_info substs))
   11.27  *)
   11.28  
   11.29 -      fun cut_and_ex_tac axiom = cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
   11.30 +      fun cut_and_ex_tac axiom =
   11.31 +        cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac @{thms exE}) 1)
   11.32        fun rotation_of_subgoal i =
   11.33          find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
   11.34  
   11.35 @@ -742,7 +743,7 @@
   11.36                THEN copy_prems_tac (map snd ax_counts) [] 1)
   11.37              THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
   11.38              THEN match_tac [prems_imp_false] 1
   11.39 -            THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i
   11.40 +            THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
   11.41                THEN rotate_tac (rotation_of_subgoal i) i
   11.42                THEN PRIMITIVE (unify_first_prem_with_concl thy i)
   11.43                THEN assume_tac i
    12.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Oct 30 21:02:01 2014 +0100
    12.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Oct 30 23:14:11 2014 +0100
    12.3 @@ -61,7 +61,7 @@
    12.4  fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
    12.5    let
    12.6      val thy = Proof_Context.theory_of ctxt
    12.7 -    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
    12.8 +    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac [refl] 1
    12.9      val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
   12.10      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   12.11    in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
   12.12 @@ -102,7 +102,7 @@
   12.13           so that "Thm.equal_elim" works below. *)
   12.14        val t0 $ _ $ t2 = prop_of eq_th
   12.15        val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
   12.16 -      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (rtac eq_th 1))
   12.17 +      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac [eq_th] 1))
   12.18      in Thm.equal_elim eq_th' th end
   12.19  
   12.20  fun clause_params ordering =
    13.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Thu Oct 30 21:02:01 2014 +0100
    13.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Thu Oct 30 23:14:11 2014 +0100
    13.3 @@ -150,7 +150,7 @@
    13.4            NONE => NONE
    13.5          | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
    13.6      val indrule' = cterm_instantiate insts indrule;
    13.7 -  in rtac indrule' i end);
    13.8 +  in resolve_tac [indrule'] i end);
    13.9  
   13.10  
   13.11  (* perform exhaustive case analysis on last parameter of subgoal i *)
    14.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Oct 30 21:02:01 2014 +0100
    14.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Oct 30 23:14:11 2014 +0100
    14.3 @@ -247,7 +247,8 @@
    14.4          val rewrites = rec_rewrites' @ map (snd o snd) defs;
    14.5        in
    14.6          map (fn eq => Goal.prove ctxt frees [] eq
    14.7 -          (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
    14.8 +          (fn {context = ctxt', ...} =>
    14.9 +            EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac [refl] 1])) eqs
   14.10        end;
   14.11    in ((prefix, (fs, defs)), prove) end
   14.12    handle PrimrecError (msg, some_eqn) =>
    15.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Oct 30 21:02:01 2014 +0100
    15.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Oct 30 23:14:11 2014 +0100
    15.3 @@ -57,10 +57,10 @@
    15.4            (Logic.strip_imp_concl t)
    15.5            (fn {prems, ...} =>
    15.6              EVERY
    15.7 -              [rtac induct' 1,
    15.8 -               REPEAT (rtac TrueI 1),
    15.9 -               REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
   15.10 -               REPEAT (rtac TrueI 1)])
   15.11 +              [resolve_tac [induct'] 1,
   15.12 +               REPEAT (resolve_tac [TrueI] 1),
   15.13 +               REPEAT ((resolve_tac [impI] 1) THEN (eresolve_tac prems 1)),
   15.14 +               REPEAT (resolve_tac [TrueI] 1)])
   15.15        end;
   15.16  
   15.17      val casedist_thms =
   15.18 @@ -176,16 +176,16 @@
   15.19            in
   15.20              (EVERY
   15.21                [DETERM tac,
   15.22 -                REPEAT (etac @{thm ex1E} 1), rtac @{thm ex1I} 1,
   15.23 +                REPEAT (eresolve_tac @{thms ex1E} 1), resolve_tac @{thms ex1I} 1,
   15.24                  DEPTH_SOLVE_1 (ares_tac [intr] 1),
   15.25 -                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
   15.26 -                etac elim 1,
   15.27 +                REPEAT_DETERM_N k (eresolve_tac [thin_rl] 1 THEN rotate_tac 1 1),
   15.28 +                eresolve_tac [elim] 1,
   15.29                  REPEAT_DETERM_N j distinct_tac,
   15.30                  TRY (dresolve_tac inject 1),
   15.31 -                REPEAT (etac conjE 1), hyp_subst_tac ctxt 1,
   15.32 -                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   15.33 +                REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1,
   15.34 +                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]),
   15.35                  TRY (hyp_subst_tac ctxt 1),
   15.36 -                rtac refl 1,
   15.37 +                resolve_tac [refl] 1,
   15.38                  REPEAT_DETERM_N (n - j - 1) distinct_tac],
   15.39                intrs, j + 1)
   15.40            end;
   15.41 @@ -211,7 +211,7 @@
   15.42            (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
   15.43            (fn {context = ctxt, ...} =>
   15.44              #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
   15.45 -              (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
   15.46 +              (((resolve_tac [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
   15.47                    rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
   15.48        end;
   15.49  
   15.50 @@ -254,10 +254,10 @@
   15.51          Goal.prove_sorry_global thy2 [] [] t
   15.52            (fn {context = ctxt, ...} => EVERY
   15.53              [rewrite_goals_tac ctxt reccomb_defs,
   15.54 -             rtac @{thm the1_equality} 1,
   15.55 +             resolve_tac @{thms the1_equality} 1,
   15.56               resolve_tac rec_unique_thms 1,
   15.57               resolve_tac rec_intrs 1,
   15.58 -             REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   15.59 +             REPEAT (resolve_tac [allI] 1 ORELSE resolve_tac rec_total_thms 1)]))
   15.60         (Old_Datatype_Prop.make_primrecs reccomb_names descr thy2);
   15.61    in
   15.62      thy2
   15.63 @@ -338,7 +338,8 @@
   15.64  
   15.65      fun prove_case t =
   15.66        Goal.prove_sorry_global thy2 [] [] t (fn {context = ctxt, ...} =>
   15.67 -        EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]);
   15.68 +        EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms),
   15.69 +          resolve_tac [refl] 1]);
   15.70  
   15.71      fun prove_cases (Type (Tcon, _)) ts =
   15.72        (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
   15.73 @@ -379,7 +380,7 @@
   15.74          val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
   15.75          val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
   15.76          fun tac ctxt =
   15.77 -          EVERY [rtac exhaustion' 1,
   15.78 +          EVERY [resolve_tac [exhaustion'] 1,
   15.79              ALLGOALS (asm_simp_tac
   15.80                (put_simpset HOL_ss ctxt addsimps (dist_rewrites' @ inject @ case_thms')))];
   15.81        in
   15.82 @@ -405,7 +406,7 @@
   15.83    let
   15.84      fun prove_case_cong_weak t =
   15.85       Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   15.86 -       (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
   15.87 +       (fn {prems, ...} => EVERY [resolve_tac [hd prems RS arg_cong] 1]);
   15.88  
   15.89      val case_cong_weaks =
   15.90        map prove_case_cong_weak (Old_Datatype_Prop.make_case_cong_weaks case_names descr thy);
   15.91 @@ -423,12 +424,13 @@
   15.92        let
   15.93          (* For goal i, select the correct disjunct to attack, then prove it *)
   15.94          fun tac ctxt i 0 =
   15.95 -              EVERY [TRY (rtac disjI1 i), hyp_subst_tac ctxt i, REPEAT (rtac exI i), rtac refl i]
   15.96 -          | tac ctxt i n = rtac disjI2 i THEN tac ctxt i (n - 1);
   15.97 +              EVERY [TRY (resolve_tac [disjI1] i), hyp_subst_tac ctxt i,
   15.98 +                REPEAT (resolve_tac [exI] i), resolve_tac [refl] i]
   15.99 +          | tac ctxt i n = resolve_tac [disjI2] i THEN tac ctxt i (n - 1);
  15.100        in
  15.101          Goal.prove_sorry_global thy [] [] t
  15.102            (fn {context = ctxt, ...} =>
  15.103 -            EVERY [rtac allI 1,
  15.104 +            EVERY [resolve_tac [allI] 1,
  15.105               Old_Datatype_Aux.exh_tac (K exhaustion) 1,
  15.106               ALLGOALS (fn i => tac ctxt i (i - 1))])
  15.107        end;
  15.108 @@ -457,8 +459,8 @@
  15.109                EVERY [
  15.110                  simp_tac (put_simpset HOL_ss ctxt addsimps [hd prems]) 1,
  15.111                  cut_tac nchotomy'' 1,
  15.112 -                REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
  15.113 -                REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
  15.114 +                REPEAT (eresolve_tac [disjE] 1 THEN REPEAT (eresolve_tac [exE] 1) THEN simplify 1),
  15.115 +                REPEAT (eresolve_tac [exE] 1) THEN simplify 1 (* Get last disjunct *)]
  15.116              end)
  15.117        end;
  15.118  
    16.1 --- a/src/HOL/Tools/cnf.ML	Thu Oct 30 21:02:01 2014 +0100
    16.2 +++ b/src/HOL/Tools/cnf.ML	Thu Oct 30 23:14:11 2014 +0100
    16.3 @@ -141,7 +141,7 @@
    16.4        if i > nprems_of thm then
    16.5          thm
    16.6        else
    16.7 -        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
    16.8 +        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (resolve_tac [clause2raw_not_disj] i) thm))
    16.9      (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
   16.10      (* becomes "[..., A1, ..., An] |- B"                                   *)
   16.11      (* Thm.thm -> Thm.thm *)
   16.12 @@ -154,7 +154,7 @@
   16.13      (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
   16.14      |> not_disj_to_prem 1
   16.15      (* [...] |- x1' ==> ... ==> xn' ==> False *)
   16.16 -    |> Seq.hd o TRYALL (rtac clause2raw_not_not)
   16.17 +    |> Seq.hd o TRYALL (resolve_tac [clause2raw_not_not])
   16.18      (* [..., x1', ..., xn'] |- False *)
   16.19      |> prems_to_hyps
   16.20    end;
   16.21 @@ -529,7 +529,7 @@
   16.22  (* ------------------------------------------------------------------------- *)
   16.23  
   16.24  fun weakening_tac i =
   16.25 -  dtac weakening_thm i THEN atac (i+1);
   16.26 +  dresolve_tac [weakening_thm] i THEN assume_tac (i+1);
   16.27  
   16.28  (* ------------------------------------------------------------------------- *)
   16.29  (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
    17.1 --- a/src/HOL/Tools/coinduction.ML	Thu Oct 30 21:02:01 2014 +0100
    17.2 +++ b/src/HOL/Tools/coinduction.ML	Thu Oct 30 23:14:11 2014 +0100
    17.3 @@ -37,7 +37,7 @@
    17.4    let
    17.5      val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
    17.6    in
    17.7 -    (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
    17.8 +    (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve_tac [thin_rl])) i st
    17.9    end;
   17.10  
   17.11  fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
   17.12 @@ -87,13 +87,15 @@
   17.13            val e = length eqs;
   17.14            val p = length prems;
   17.15          in
   17.16 -          HEADGOAL (EVERY' [rtac thm,
   17.17 +          HEADGOAL (EVERY' [resolve_tac [thm],
   17.18              EVERY' (map (fn var =>
   17.19 -              rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
   17.20 -            if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
   17.21 -            else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
   17.22 +              resolve_tac [cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI]) vars),
   17.23 +            if p = 0 then CONJ_WRAP' (K (resolve_tac [refl])) eqs
   17.24 +            else
   17.25 +              REPEAT_DETERM_N e o (resolve_tac [conjI] THEN' resolve_tac [refl]) THEN'
   17.26 +              CONJ_WRAP' (resolve_tac o single) prems,
   17.27              K (ALLGOALS_SKIP skip
   17.28 -               (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
   17.29 +               (REPEAT_DETERM_N (length vars) o (eresolve_tac [exE] THEN' rotate_tac ~1) THEN'
   17.30                 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
   17.31                   (case prems of
   17.32                     [] => all_tac
    18.1 --- a/src/HOL/Tools/inductive.ML	Thu Oct 30 21:02:01 2014 +0100
    18.2 +++ b/src/HOL/Tools/inductive.ML	Thu Oct 30 23:14:11 2014 +0100
    18.3 @@ -169,8 +169,8 @@
    18.4    | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
    18.5  
    18.6  fun select_disj 1 1 = []
    18.7 -  | select_disj _ 1 = [rtac disjI1]
    18.8 -  | select_disj n i = rtac disjI2 :: select_disj (n - 1) (i - 1);
    18.9 +  | select_disj _ 1 = [resolve_tac [disjI1]]
   18.10 +  | select_disj n i = resolve_tac [disjI2] :: select_disj (n - 1) (i - 1);
   18.11  
   18.12  
   18.13  
   18.14 @@ -378,12 +378,13 @@
   18.15      [] []
   18.16      (HOLogic.mk_Trueprop
   18.17        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
   18.18 -    (fn _ => EVERY [rtac @{thm monoI} 1,
   18.19 +    (fn _ => EVERY [resolve_tac @{thms monoI} 1,
   18.20        REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
   18.21        REPEAT (FIRST
   18.22 -        [atac 1,
   18.23 +        [assume_tac 1,
   18.24           resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
   18.25 -         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
   18.26 +         eresolve_tac @{thms le_funE} 1,
   18.27 +         dresolve_tac @{thms le_boolD} 1])]));
   18.28  
   18.29  
   18.30  (* prove introduction rules *)
   18.31 @@ -401,7 +402,7 @@
   18.32      val intrs = map_index (fn (i, intr) =>
   18.33        Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
   18.34         [rewrite_goals_tac ctxt rec_preds_defs,
   18.35 -        rtac (unfold RS iffD2) 1,
   18.36 +        resolve_tac [unfold RS iffD2] 1,
   18.37          EVERY1 (select_disj (length intr_ts) (i + 1)),
   18.38          (*Not ares_tac, since refl must be tried before any equality assumptions;
   18.39            backtracking may occur if the premises have extra variables!*)
   18.40 @@ -447,7 +448,7 @@
   18.41            (fn {context = ctxt4, prems} => EVERY
   18.42              [cut_tac (hd prems) 1,
   18.43               rewrite_goals_tac ctxt4 rec_preds_defs,
   18.44 -             dtac (unfold RS iffD1) 1,
   18.45 +             dresolve_tac [unfold RS iffD1] 1,
   18.46               REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   18.47               REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   18.48               EVERY (map (fn prem =>
   18.49 @@ -494,37 +495,39 @@
   18.50          val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   18.51          fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   18.52              EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
   18.53 -            EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
   18.54 -            (if null prems then rtac @{thm TrueI} 1
   18.55 +            EVERY (replicate (length params) (resolve_tac @{thms exI} 1)) THEN
   18.56 +            (if null prems then resolve_tac @{thms TrueI} 1
   18.57               else
   18.58                let
   18.59                  val (prems', last_prem) = split_last prems;
   18.60                in
   18.61 -                EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
   18.62 -                rtac last_prem 1
   18.63 +                EVERY (map (fn prem =>
   18.64 +                  (resolve_tac @{thms conjI} 1 THEN resolve_tac [prem] 1)) prems') THEN
   18.65 +                resolve_tac [last_prem] 1
   18.66                end)) ctxt' 1;
   18.67          fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
   18.68 -          EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
   18.69 -          (if null ts andalso null us then rtac intr 1
   18.70 +          EVERY (replicate (length params') (eresolve_tac @{thms exE} 1)) THEN
   18.71 +          (if null ts andalso null us then resolve_tac [intr] 1
   18.72             else
   18.73 -            EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
   18.74 +            EVERY (replicate (length ts + length us - 1) (eresolve_tac @{thms conjE} 1)) THEN
   18.75              Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
   18.76                let
   18.77                  val (eqs, prems') = chop (length us) prems;
   18.78                  val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
   18.79                in
   18.80                  rewrite_goal_tac ctxt'' rew_thms 1 THEN
   18.81 -                rtac intr 1 THEN
   18.82 -                EVERY (map (fn p => rtac p 1) prems')
   18.83 +                resolve_tac [intr] 1 THEN
   18.84 +                EVERY (map (fn p => resolve_tac [p] 1) prems')
   18.85                end) ctxt' 1);
   18.86        in
   18.87          Goal.prove_sorry ctxt' [] [] eq (fn _ =>
   18.88 -          rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN
   18.89 +          resolve_tac @{thms iffI} 1 THEN
   18.90 +          eresolve_tac [#1 elim] 1 THEN
   18.91            EVERY (map_index prove_intr1 c_intrs) THEN
   18.92 -          (if null c_intrs then etac @{thm FalseE} 1
   18.93 +          (if null c_intrs then eresolve_tac @{thms FalseE} 1
   18.94             else
   18.95              let val (c_intrs', last_c_intr) = split_last c_intrs in
   18.96 -              EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
   18.97 +              EVERY (map (fn ci => eresolve_tac @{thms disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
   18.98                prove_intr2 last_c_intr
   18.99              end))
  18.100          |> rulify ctxt'
  18.101 @@ -729,16 +732,16 @@
  18.102      val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
  18.103        (fn {context = ctxt3, prems} => EVERY
  18.104          [rewrite_goals_tac ctxt3 [inductive_conj_def],
  18.105 -         DETERM (rtac raw_fp_induct 1),
  18.106 +         DETERM (resolve_tac [raw_fp_induct] 1),
  18.107           REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
  18.108           rewrite_goals_tac ctxt3 simp_thms2,
  18.109           (*This disjE separates out the introduction rules*)
  18.110           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
  18.111           (*Now break down the individual cases.  No disjE here in case
  18.112             some premise involves disjunction.*)
  18.113 -         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
  18.114 +         REPEAT (FIRSTGOAL (eresolve_tac [conjE] ORELSE' bound_hyp_subst_tac ctxt3)),
  18.115           REPEAT (FIRSTGOAL
  18.116 -           (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
  18.117 +           (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac))),
  18.118           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
  18.119               (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
  18.120             conjI, refl] 1)) prems)]);
  18.121 @@ -749,9 +752,9 @@
  18.122           REPEAT (EVERY
  18.123             [REPEAT (resolve_tac [conjI, impI] 1),
  18.124              REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
  18.125 -            atac 1,
  18.126 +            assume_tac 1,
  18.127              rewrite_goals_tac ctxt3 simp_thms1,
  18.128 -            atac 1])]);
  18.129 +            assume_tac 1])]);
  18.130  
  18.131    in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
  18.132  
    19.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Oct 30 21:02:01 2014 +0100
    19.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Oct 30 23:14:11 2014 +0100
    19.3 @@ -75,11 +75,14 @@
    19.4                SOME (close (Goal.prove ctxt [] [])
    19.5                  (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
    19.6                  (K (EVERY
    19.7 -                  [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1,
    19.8 -                   EVERY [etac conjE 1, rtac IntI 1, simp, simp,
    19.9 -                     etac IntE 1, rtac conjI 1, simp, simp] ORELSE
   19.10 -                   EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp,
   19.11 -                     etac UnE 1, rtac disjI1 1, simp, rtac disjI2 1, simp]])))
   19.12 +                  [resolve_tac [eq_reflection] 1, REPEAT (resolve_tac @{thms ext} 1),
   19.13 +                   resolve_tac [iffI] 1,
   19.14 +                   EVERY [eresolve_tac [conjE] 1, resolve_tac [IntI] 1, simp, simp,
   19.15 +                     eresolve_tac [IntE] 1, resolve_tac [conjI] 1, simp, simp] ORELSE
   19.16 +                   EVERY [eresolve_tac [disjE] 1, resolve_tac [UnI1] 1, simp,
   19.17 +                     resolve_tac [UnI2] 1, simp,
   19.18 +                     eresolve_tac [UnE] 1, resolve_tac [disjI1] 1, simp,
   19.19 +                     resolve_tac [disjI2] 1, simp]])))
   19.20                  handle ERROR _ => NONE))
   19.21      in
   19.22        case strip_comb t of
   19.23 @@ -502,8 +505,9 @@
   19.24                 fold_rev (Term.abs o pair "x") Ts
   19.25                  (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
   19.26                    list_comb (c, params))))))
   19.27 -            (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
   19.28 -              [def, mem_Collect_eq, @{thm split_conv}]) 1))
   19.29 +            (K (REPEAT (resolve_tac @{thms ext} 1) THEN
   19.30 +              simp_tac (put_simpset HOL_basic_ss lthy addsimps
   19.31 +                [def, mem_Collect_eq, @{thm split_conv}]) 1))
   19.32          in
   19.33            lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
   19.34              [Attrib.internal (K pred_set_conv_att)]),
    20.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Oct 30 21:02:01 2014 +0100
    20.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Oct 30 23:14:11 2014 +0100
    20.3 @@ -731,11 +731,11 @@
    20.4        end)
    20.5    in
    20.6      EVERY' [
    20.7 -      REPEAT_DETERM o etac rev_mp,
    20.8 +      REPEAT_DETERM o eresolve_tac [rev_mp],
    20.9        cond_split_tac,
   20.10 -      rtac @{thm ccontr},
   20.11 +      resolve_tac @{thms ccontr},
   20.12        prem_nnf_tac ctxt,
   20.13 -      TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
   20.14 +      TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' eresolve_tac [disjE]))
   20.15      ]
   20.16    end;
   20.17  
   20.18 @@ -758,7 +758,7 @@
   20.19              THEN_ALL_NEW
   20.20                (CONVERSION Drule.beta_eta_conversion
   20.21                  THEN'
   20.22 -              (TRY o (etac notE THEN' eq_assume_tac)))
   20.23 +              (TRY o (eresolve_tac [notE] THEN' eq_assume_tac)))
   20.24          ) i
   20.25      )
   20.26    end;
   20.27 @@ -835,11 +835,12 @@
   20.28          REPEAT_DETERM
   20.29                (eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE
   20.30                 filter_prems_tac test 1 ORELSE
   20.31 -               etac @{thm disjE} 1) THEN
   20.32 -        (DETERM (etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
   20.33 +               eresolve_tac @{thms disjE} 1) THEN
   20.34 +        (DETERM (eresolve_tac @{thms notE} 1 THEN eq_assume_tac 1) ORELSE
   20.35           ref_tac 1);
   20.36    in EVERY'[TRY o filter_prems_tac test,
   20.37 -            REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac ctxt,
   20.38 +            REPEAT_DETERM o eresolve_tac @{thms rev_mp}, prep_tac,
   20.39 +              resolve_tac @{thms ccontr}, prem_nnf_tac ctxt,
   20.40              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   20.41    end;
   20.42  
   20.43 @@ -872,7 +873,8 @@
   20.44  
   20.45  fun gen_tac ex ctxt =
   20.46    FIRST' [simple_tac ctxt,
   20.47 -    Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
   20.48 +    Object_Logic.full_atomize_tac ctxt THEN'
   20.49 +    (REPEAT_DETERM o resolve_tac [impI]) THEN' raw_tac ctxt ex];
   20.50  
   20.51  val tac = gen_tac true;
   20.52  
    21.1 --- a/src/HOL/Tools/sat.ML	Thu Oct 30 21:02:01 2014 +0100
    21.2 +++ b/src/HOL/Tools/sat.ML	Thu Oct 30 23:14:11 2014 +0100
    21.3 @@ -406,7 +406,7 @@
    21.4  
    21.5  fun rawsat_tac ctxt i =
    21.6    Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
    21.7 -    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
    21.8 +    resolve_tac [rawsat_thm ctxt' (map cprop_of prems)] 1) ctxt i;
    21.9  
   21.10  (* ------------------------------------------------------------------------- *)
   21.11  (* pre_cnf_tac: converts the i-th subgoal                                    *)
   21.12 @@ -421,7 +421,7 @@
   21.13  (* ------------------------------------------------------------------------- *)
   21.14  
   21.15  fun pre_cnf_tac ctxt =
   21.16 -  rtac @{thm ccontr} THEN'
   21.17 +  resolve_tac @{thms ccontr} THEN'
   21.18    Object_Logic.atomize_prems_tac ctxt THEN'
   21.19    CONVERSION Drule.beta_eta_conversion;
   21.20  
   21.21 @@ -433,7 +433,7 @@
   21.22  (* ------------------------------------------------------------------------- *)
   21.23  
   21.24  fun cnfsat_tac ctxt i =
   21.25 -  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
   21.26 +  (eresolve_tac [FalseE] i) ORELSE (REPEAT_DETERM (eresolve_tac [conjE] i) THEN rawsat_tac ctxt i);
   21.27  
   21.28  (* ------------------------------------------------------------------------- *)
   21.29  (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   21.30 @@ -443,8 +443,8 @@
   21.31  (* ------------------------------------------------------------------------- *)
   21.32  
   21.33  fun cnfxsat_tac ctxt i =
   21.34 -  (etac FalseE i) ORELSE
   21.35 -    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
   21.36 +  (eresolve_tac [FalseE] i) ORELSE
   21.37 +    (REPEAT_DETERM (eresolve_tac [conjE] i ORELSE eresolve_tac [exE] i) THEN rawsat_tac ctxt i);
   21.38  
   21.39  (* ------------------------------------------------------------------------- *)
   21.40  (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
    22.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 30 21:02:01 2014 +0100
    22.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 30 23:14:11 2014 +0100
    22.3 @@ -314,95 +314,96 @@
    22.4  val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
    22.5  val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
    22.6  
    22.7 -fun elim_Collect_tac ctxt = dtac @{thm iffD1[OF mem_Collect_eq]}
    22.8 +fun elim_Collect_tac ctxt = dresolve_tac @{thms iffD1 [OF mem_Collect_eq]}
    22.9    THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
   22.10 -  THEN' REPEAT_DETERM o etac @{thm conjE}
   22.11 +  THEN' REPEAT_DETERM o eresolve_tac @{thms conjE}
   22.12    THEN' TRY o hyp_subst_tac ctxt;
   22.13  
   22.14 -fun intro_image_tac ctxt = rtac @{thm image_eqI}
   22.15 +fun intro_image_tac ctxt = resolve_tac @{thms image_eqI}
   22.16      THEN' (REPEAT_DETERM1 o
   22.17 -      (rtac @{thm refl}
   22.18 -      ORELSE' rtac
   22.19 -        @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]}
   22.20 +      (resolve_tac @{thms refl}
   22.21 +      ORELSE' resolve_tac @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
   22.22        ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
   22.23          (HOLogic.Trueprop_conv
   22.24            (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
   22.25  
   22.26 -fun elim_image_tac ctxt = etac @{thm imageE}
   22.27 +fun elim_image_tac ctxt = eresolve_tac @{thms imageE}
   22.28    THEN' REPEAT_DETERM o CHANGED o
   22.29      (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
   22.30 -    THEN' REPEAT_DETERM o etac @{thm Pair_inject}
   22.31 +    THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
   22.32      THEN' TRY o hyp_subst_tac ctxt)
   22.33  
   22.34  fun tac1_of_formula ctxt (Int (fm1, fm2)) =
   22.35 -    TRY o etac @{thm conjE}
   22.36 -    THEN' rtac @{thm IntI}
   22.37 +    TRY o eresolve_tac @{thms conjE}
   22.38 +    THEN' resolve_tac @{thms IntI}
   22.39      THEN' (fn i => tac1_of_formula ctxt fm2 (i + 1))
   22.40      THEN' tac1_of_formula ctxt fm1
   22.41    | tac1_of_formula ctxt (Un (fm1, fm2)) =
   22.42 -    etac @{thm disjE} THEN' rtac @{thm UnI1}
   22.43 +    eresolve_tac @{thms disjE} THEN' resolve_tac @{thms UnI1}
   22.44      THEN' tac1_of_formula ctxt fm1
   22.45 -    THEN' rtac @{thm UnI2}
   22.46 +    THEN' resolve_tac @{thms UnI2}
   22.47      THEN' tac1_of_formula ctxt fm2
   22.48    | tac1_of_formula ctxt (Atom _) =
   22.49 -    REPEAT_DETERM1 o (atac
   22.50 -      ORELSE' rtac @{thm SigmaI}
   22.51 -      ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN'
   22.52 +    REPEAT_DETERM1 o (assume_tac
   22.53 +      ORELSE' resolve_tac @{thms SigmaI}
   22.54 +      ORELSE' ((resolve_tac @{thms CollectI} ORELSE' resolve_tac [collectI']) THEN'
   22.55          TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
   22.56 -      ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
   22.57 +      ORELSE' ((resolve_tac @{thms vimageI2} ORELSE' resolve_tac [vimageI2']) THEN'
   22.58          TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
   22.59 -      ORELSE' (rtac @{thm image_eqI} THEN'
   22.60 +      ORELSE' (resolve_tac @{thms image_eqI} THEN'
   22.61      (REPEAT_DETERM o
   22.62 -      (rtac @{thm refl}
   22.63 -      ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]})))
   22.64 -      ORELSE' rtac @{thm UNIV_I}
   22.65 -      ORELSE' rtac @{thm iffD2[OF Compl_iff]}
   22.66 -      ORELSE' atac)
   22.67 +      (resolve_tac @{thms refl}
   22.68 +      ORELSE' resolve_tac @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]})))
   22.69 +      ORELSE' resolve_tac @{thms UNIV_I}
   22.70 +      ORELSE' resolve_tac @{thms iffD2[OF Compl_iff]}
   22.71 +      ORELSE' assume_tac)
   22.72  
   22.73  fun tac2_of_formula ctxt (Int (fm1, fm2)) =
   22.74 -    TRY o etac @{thm IntE}
   22.75 -    THEN' TRY o rtac @{thm conjI}
   22.76 +    TRY o eresolve_tac @{thms IntE}
   22.77 +    THEN' TRY o resolve_tac @{thms conjI}
   22.78      THEN' (fn i => tac2_of_formula ctxt fm2 (i + 1))
   22.79      THEN' tac2_of_formula ctxt fm1
   22.80    | tac2_of_formula ctxt (Un (fm1, fm2)) =
   22.81 -    etac @{thm UnE} THEN' rtac @{thm disjI1}
   22.82 +    eresolve_tac @{thms UnE} THEN' resolve_tac @{thms disjI1}
   22.83      THEN' tac2_of_formula ctxt fm1
   22.84 -    THEN' rtac @{thm disjI2}
   22.85 +    THEN' resolve_tac @{thms disjI2}
   22.86      THEN' tac2_of_formula ctxt fm2
   22.87    | tac2_of_formula ctxt (Atom _) =
   22.88      REPEAT_DETERM o
   22.89 -      (atac
   22.90 -       ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}
   22.91 -       ORELSE' etac @{thm conjE}
   22.92 -       ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
   22.93 +      (assume_tac
   22.94 +       ORELSE' dresolve_tac @{thms iffD1[OF mem_Sigma_iff]}
   22.95 +       ORELSE' eresolve_tac @{thms conjE}
   22.96 +       ORELSE' ((eresolve_tac @{thms CollectE} ORELSE' eresolve_tac [collectE']) THEN'
   22.97           TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN'
   22.98 -         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
   22.99 -       ORELSE' (etac @{thm imageE}
  22.100 +         REPEAT_DETERM o eresolve_tac @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN'
  22.101 +         TRY o resolve_tac @{thms refl})
  22.102 +       ORELSE' (eresolve_tac @{thms imageE}
  22.103           THEN' (REPEAT_DETERM o CHANGED o
  22.104           (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
  22.105 -         THEN' REPEAT_DETERM o etac @{thm Pair_inject}
  22.106 -         THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
  22.107 -       ORELSE' etac @{thm ComplE}
  22.108 -       ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
  22.109 +         THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
  22.110 +         THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl})))
  22.111 +       ORELSE' eresolve_tac @{thms ComplE}
  22.112 +       ORELSE' ((eresolve_tac @{thms vimageE} ORELSE' eresolve_tac [vimageE'])
  22.113          THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])
  22.114 -        THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
  22.115 +        THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl}))
  22.116  
  22.117  fun tac ctxt fm =
  22.118    let
  22.119 -    val subset_tac1 = rtac @{thm subsetI}
  22.120 +    val subset_tac1 = resolve_tac @{thms subsetI}
  22.121        THEN' elim_Collect_tac ctxt
  22.122        THEN' intro_image_tac ctxt
  22.123        THEN' tac1_of_formula ctxt fm
  22.124 -    val subset_tac2 = rtac @{thm subsetI}
  22.125 +    val subset_tac2 = resolve_tac @{thms subsetI}
  22.126        THEN' elim_image_tac ctxt
  22.127 -      THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
  22.128 +      THEN' resolve_tac @{thms iffD2[OF mem_Collect_eq]}
  22.129        THEN' REPEAT_DETERM o resolve_tac @{thms exI}
  22.130 -      THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
  22.131 -      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' rtac @{thm refl}))))
  22.132 +      THEN' (TRY o REPEAT_ALL_NEW (resolve_tac @{thms conjI}))
  22.133 +      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' resolve_tac @{thms refl}))))
  22.134        THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
  22.135 -        REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
  22.136 +        REPEAT_DETERM (eresolve_tac @{thms IntE} (i + j)) THEN
  22.137 +        tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
  22.138    in
  22.139 -    rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
  22.140 +    resolve_tac @{thms subset_antisym} THEN' subset_tac1 THEN' subset_tac2
  22.141    end;
  22.142  
  22.143  
  22.144 @@ -429,18 +430,18 @@
  22.145      fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
  22.146      val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
  22.147      fun tac ctxt = 
  22.148 -      rtac @{thm set_eqI}
  22.149 +      resolve_tac @{thms set_eqI}
  22.150        THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
  22.151 -      THEN' rtac @{thm iffI}
  22.152 -      THEN' REPEAT_DETERM o rtac @{thm exI}
  22.153 -      THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac
  22.154 -      THEN' REPEAT_DETERM o etac @{thm exE}
  22.155 -      THEN' etac @{thm conjE}
  22.156 -      THEN' REPEAT_DETERM o etac @{thm Pair_inject}
  22.157 +      THEN' resolve_tac @{thms iffI}
  22.158 +      THEN' REPEAT_DETERM o resolve_tac @{thms exI}
  22.159 +      THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac
  22.160 +      THEN' REPEAT_DETERM o eresolve_tac @{thms exE}
  22.161 +      THEN' eresolve_tac @{thms conjE}
  22.162 +      THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
  22.163        THEN' Subgoal.FOCUS (fn {prems, ...} =>
  22.164          (* FIXME inner context!? *)
  22.165          simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
  22.166 -      THEN' TRY o atac
  22.167 +      THEN' TRY o assume_tac
  22.168    in
  22.169      case try mk_term (term_of ct) of
  22.170        NONE => Thm.reflexive ct
    23.1 --- a/src/HOL/Tools/simpdata.ML	Thu Oct 30 21:02:01 2014 +0100
    23.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Oct 30 23:14:11 2014 +0100
    23.3 @@ -81,7 +81,7 @@
    23.4  (*Congruence rules for = (instead of ==)*)
    23.5  fun mk_meta_cong (_: Proof.context) rl = zero_var_indexes
    23.6    (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
    23.7 -     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    23.8 +     resolve_tac [lift_meta_eq_to_obj_eq i st] i st) rl)
    23.9     in mk_meta_eq rl' handle THM _ =>
   23.10       if can Logic.dest_equals (concl_of rl') then rl'
   23.11       else error "Conclusion of congruence rules must be =-equality"
   23.12 @@ -119,7 +119,7 @@
   23.13      val sol_thms =
   23.14        reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
   23.15      fun sol_tac i =
   23.16 -      FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE
   23.17 +      FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
   23.18        (match_tac intros THEN_ALL_NEW sol_tac) i
   23.19    in
   23.20      (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
    24.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 21:02:01 2014 +0100
    24.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 23:14:11 2014 +0100
    24.3 @@ -92,12 +92,12 @@
    24.4      Option.map (export o Data.simplify_meta_eq ctxt)
    24.5        (if n2 <= n1 then
    24.6           Data.prove_conv
    24.7 -           [Data.trans_tac reshape, rtac Data.bal_add1 1,
    24.8 +           [Data.trans_tac reshape, resolve_tac [Data.bal_add1] 1,
    24.9              Data.numeral_simp_tac ctxt] ctxt prems
   24.10             (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
   24.11         else
   24.12           Data.prove_conv
   24.13 -           [Data.trans_tac reshape, rtac Data.bal_add2 1,
   24.14 +           [Data.trans_tac reshape, resolve_tac [Data.bal_add2] 1,
   24.15              Data.numeral_simp_tac ctxt] ctxt prems
   24.16             (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
   24.17    end
    25.1 --- a/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 21:02:01 2014 +0100
    25.2 +++ b/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 23:14:11 2014 +0100
    25.3 @@ -83,7 +83,7 @@
    25.4    in
    25.5      Option.map (export o Data.simplify_meta_eq ctxt)
    25.6        (Data.prove_conv
    25.7 -         [Data.trans_tac reshape, rtac Data.left_distrib 1,
    25.8 +         [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1,
    25.9            Data.numeral_simp_tac ctxt] ctxt
   25.10           (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   25.11    end
    26.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 30 21:02:01 2014 +0100
    26.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 30 23:14:11 2014 +0100
    26.3 @@ -815,7 +815,7 @@
    26.4            all_tac) THEN
    26.5            PRIMITIVE (trace_thm ctxt ["State after neqE:"]) THEN
    26.6            (* use theorems generated from the actual justifications *)
    26.7 -          Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ctxt prems j) 1) ctxt i
    26.8 +          Subgoal.FOCUS (fn {prems, ...} => resolve_tac [mkthm ctxt prems j] 1) ctxt i
    26.9      in
   26.10        (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
   26.11        DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
    27.1 --- a/src/Provers/blast.ML	Thu Oct 30 21:02:01 2014 +0100
    27.2 +++ b/src/Provers/blast.ML	Thu Oct 30 23:14:11 2014 +0100
    27.3 @@ -488,8 +488,8 @@
    27.4  
    27.5  (*Resolution/matching tactics: if upd then the proof state may be updated.
    27.6    Matching makes the tactics more deterministic in the presence of Vars.*)
    27.7 -fun emtac ctxt upd rl = TRACE ctxt rl (if upd then etac rl else ematch_tac [rl]);
    27.8 -fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then rtac rl else match_tac [rl]);
    27.9 +fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]);
   27.10 +fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]);
   27.11  
   27.12  (*Tableau rule from elimination rule.
   27.13    Flag "upd" says that the inference updated the branch.
   27.14 @@ -624,7 +624,7 @@
   27.15  
   27.16  (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
   27.17  fun negOfGoal_tac ctxt i =
   27.18 -  TRACE ctxt Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i;
   27.19 +  TRACE ctxt Data.ccontr (resolve_tac [Data.ccontr]) i THEN rotate_tac ~1 i;
   27.20  
   27.21  fun traceTerm ctxt t =
   27.22    let val thy = Proof_Context.theory_of ctxt
    28.1 --- a/src/Provers/classical.ML	Thu Oct 30 21:02:01 2014 +0100
    28.2 +++ b/src/Provers/classical.ML	Thu Oct 30 23:14:11 2014 +0100
    28.3 @@ -157,7 +157,7 @@
    28.4        val rule'' =
    28.5          rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
    28.6            if i = 1 orelse redundant_hyp goal
    28.7 -          then etac thin_rl i
    28.8 +          then eresolve_tac [thin_rl] i
    28.9            else all_tac))
   28.10          |> Seq.hd
   28.11          |> Drule.zero_var_indexes;
   28.12 @@ -209,7 +209,7 @@
   28.13    let
   28.14      val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
   28.15      val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
   28.16 -  in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
   28.17 +  in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end;
   28.18  
   28.19  
   28.20  (**** Classical rule sets ****)
   28.21 @@ -689,8 +689,8 @@
   28.22  fun ctxt addafter (name, tac2) =
   28.23    ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
   28.24  
   28.25 -fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dtac thm THEN' assume_tac);
   28.26 -fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => etac thm THEN' assume_tac);
   28.27 +fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
   28.28 +fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
   28.29  fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
   28.30  fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
   28.31  
   28.32 @@ -909,7 +909,7 @@
   28.33      val ruleq = Drule.multi_resolves facts rules;
   28.34      val _ = Method.trace ctxt rules;
   28.35    in
   28.36 -    fn st => Seq.maps (fn rule => rtac rule i st) ruleq
   28.37 +    fn st => Seq.maps (fn rule => resolve_tac [rule] i st) ruleq
   28.38    end)
   28.39    THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
   28.40  
    29.1 --- a/src/Provers/hypsubst.ML	Thu Oct 30 21:02:01 2014 +0100
    29.2 +++ b/src/Provers/hypsubst.ML	Thu Oct 30 23:14:11 2014 +0100
    29.3 @@ -126,7 +126,7 @@
    29.4       val (k, _) = eq_var false false false t
    29.5       val ok = (eq_var false false true t |> fst) > k
    29.6          handle EQ_VAR => true
    29.7 -   in if ok then EVERY [rotate_tac k i, etac thin_rl i, rotate_tac (~k) i]
    29.8 +   in if ok then EVERY [rotate_tac k i, eresolve_tac [thin_rl] i, rotate_tac (~k) i]
    29.9      else no_tac
   29.10     end handle EQ_VAR => no_tac)
   29.11  
   29.12 @@ -151,11 +151,11 @@
   29.13          val (k, (orient, is_free)) = eq_var bnd true true Bi
   29.14          val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
   29.15        in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
   29.16 -        if not is_free then etac thin_rl i
   29.17 -          else if orient then etac Data.rev_mp i
   29.18 -          else etac (Data.sym RS Data.rev_mp) i,
   29.19 +        if not is_free then eresolve_tac [thin_rl] i
   29.20 +          else if orient then eresolve_tac [Data.rev_mp] i
   29.21 +          else eresolve_tac [Data.sym RS Data.rev_mp] i,
   29.22          rotate_tac (~k) i,
   29.23 -        if is_free then rtac Data.imp_intr i else all_tac]
   29.24 +        if is_free then resolve_tac [Data.imp_intr] i else all_tac]
   29.25        end handle THM _ => no_tac | EQ_VAR => no_tac)
   29.26  
   29.27  end;
   29.28 @@ -194,7 +194,7 @@
   29.29        end
   29.30    | NONE => no_tac);
   29.31  
   29.32 -val imp_intr_tac = rtac Data.imp_intr;
   29.33 +val imp_intr_tac = resolve_tac [Data.imp_intr];
   29.34  
   29.35  fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
   29.36  val dup_subst = rev_dup_elim ssubst
   29.37 @@ -211,9 +211,9 @@
   29.38            val rl = if orient then rl else Data.sym RS rl
   29.39        in
   29.40           DETERM
   29.41 -           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   29.42 +           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
   29.43                     rotate_tac 1 i,
   29.44 -                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   29.45 +                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
   29.46                     inst_subst_tac orient rl i,
   29.47                     REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   29.48        end
   29.49 @@ -245,7 +245,7 @@
   29.50  fun reverse_n_tac 0 i = all_tac
   29.51    | reverse_n_tac 1 i = rotate_tac ~1 i
   29.52    | reverse_n_tac n i =
   29.53 -      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
   29.54 +      REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac [Data.rev_mp] i) THEN
   29.55        REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   29.56  
   29.57  (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   29.58 @@ -279,9 +279,9 @@
   29.59        in
   29.60           if trace then tracing "Substituting an equality" else ();
   29.61           DETERM
   29.62 -           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   29.63 +           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
   29.64                     rotate_tac 1 i,
   29.65 -                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   29.66 +                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
   29.67                     inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
   29.68                     all_imp_intr_tac hyps i])
   29.69        end
   29.70 @@ -291,7 +291,7 @@
   29.71    fails unless the substitution has an effect*)
   29.72  fun stac th =
   29.73    let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   29.74 -  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   29.75 +  in CHANGED_GOAL (resolve_tac [th' RS ssubst]) end;
   29.76  
   29.77  
   29.78  (* method setup *)
    30.1 --- a/src/Provers/order.ML	Thu Oct 30 21:02:01 2014 +0100
    30.2 +++ b/src/Provers/order.ML	Thu Oct 30 23:14:11 2014 +0100
    30.3 @@ -1243,10 +1243,10 @@
    30.4    in
    30.5     Subgoal.FOCUS (fn {prems = asms, ...} =>
    30.6       let val thms = map (prove (prems @ asms)) prfs
    30.7 -     in rtac (prove thms prf) 1 end) ctxt n st
    30.8 +     in resolve_tac [prove thms prf] 1 end) ctxt n st
    30.9    end
   30.10    handle Contr p =>
   30.11 -      (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
   30.12 +      (Subgoal.FOCUS (fn {prems = asms, ...} => resolve_tac [prove asms p] 1) ctxt n st
   30.13          handle General.Subscript => Seq.empty)
   30.14     | Cannot => Seq.empty
   30.15     | General.Subscript => Seq.empty)
    31.1 --- a/src/Provers/quantifier1.ML	Thu Oct 30 21:02:01 2014 +0100
    31.2 +++ b/src/Provers/quantifier1.ML	Thu Oct 30 23:14:11 2014 +0100
    31.3 @@ -126,10 +126,10 @@
    31.4        yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
    31.5      val thm =
    31.6        Goal.prove ctxt' [] [] goal
    31.7 -        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
    31.8 +        (fn {context = ctxt'', ...} => resolve_tac [Data.iff_reflection] 1 THEN tac ctxt'');
    31.9    in singleton (Variable.export ctxt' ctxt) thm end;
   31.10  
   31.11 -fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
   31.12 +fun qcomm_tac qcomm qI i = REPEAT_DETERM (resolve_tac [qcomm] i THEN resolve_tac [qI] i);
   31.13  
   31.14  (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
   31.15     Better: instantiate exI
   31.16 @@ -138,9 +138,10 @@
   31.17    val excomm = Data.ex_comm RS Data.iff_trans;
   31.18  in
   31.19    val prove_one_point_ex_tac =
   31.20 -    qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
   31.21 +    qcomm_tac excomm Data.iff_exI 1 THEN resolve_tac [Data.iffI] 1 THEN
   31.22      ALLGOALS
   31.23 -      (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI,
   31.24 +      (EVERY' [eresolve_tac [Data.exE], REPEAT_DETERM o eresolve_tac [Data.conjE],
   31.25 +        resolve_tac [Data.exI],
   31.26          DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
   31.27  end;
   31.28  
   31.29 @@ -150,12 +151,17 @@
   31.30  local
   31.31    val tac =
   31.32      SELECT_GOAL
   31.33 -      (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp,
   31.34 -        REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]);
   31.35 +      (EVERY1 [REPEAT o dresolve_tac [Data.uncurry],
   31.36 +        REPEAT o resolve_tac [Data.impI],
   31.37 +        eresolve_tac [Data.mp],
   31.38 +        REPEAT o eresolve_tac [Data.conjE],
   31.39 +        REPEAT o ares_tac [Data.conjI]]);
   31.40    val allcomm = Data.all_comm RS Data.iff_trans;
   31.41  in
   31.42    val prove_one_point_all_tac =
   31.43 -    EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac];
   31.44 +    EVERY1 [qcomm_tac allcomm Data.iff_allI,
   31.45 +      resolve_tac [Data.iff_allI],
   31.46 +      resolve_tac [Data.iffI], tac, tac];
   31.47  end
   31.48  
   31.49  fun renumber l u (Bound i) =
    32.1 --- a/src/Provers/quasi.ML	Thu Oct 30 21:02:01 2014 +0100
    32.2 +++ b/src/Provers/quasi.ML	Thu Oct 30 23:14:11 2014 +0100
    32.3 @@ -565,9 +565,9 @@
    32.4   in
    32.5    Subgoal.FOCUS (fn {prems, ...} =>
    32.6      let val thms = map (prove prems) prfs
    32.7 -    in rtac (prove thms prf) 1 end) ctxt n st
    32.8 +    in resolve_tac [prove thms prf] 1 end) ctxt n st
    32.9   end
   32.10 - handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   32.11 + handle Contr p => Subgoal.FOCUS (fn {prems, ...} => resolve_tac [prove prems p] 1) ctxt n st
   32.12    | Cannot  => Seq.empty);
   32.13  
   32.14  
   32.15 @@ -585,10 +585,10 @@
   32.16   in
   32.17    Subgoal.FOCUS (fn {prems, ...} =>
   32.18      let val thms = map (prove prems) prfs
   32.19 -    in rtac (prove thms prf) 1 end) ctxt n st
   32.20 +    in resolve_tac [prove thms prf] 1 end) ctxt n st
   32.21   end
   32.22   handle Contr p =>
   32.23 -    (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   32.24 +    (Subgoal.FOCUS (fn {prems, ...} => resolve_tac [prove prems p] 1) ctxt n st
   32.25        handle General.Subscript => Seq.empty)
   32.26    | Cannot => Seq.empty
   32.27    | General.Subscript => Seq.empty);
    33.1 --- a/src/Provers/splitter.ML	Thu Oct 30 21:02:01 2014 +0100
    33.2 +++ b/src/Provers/splitter.ML	Thu Oct 30 23:14:11 2014 +0100
    33.3 @@ -99,7 +99,7 @@
    33.4  val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
    33.5    [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
    33.6    (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
    33.7 -  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
    33.8 +  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN resolve_tac [reflexive_thm] 1)
    33.9  
   33.10  val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
   33.11  
   33.12 @@ -365,11 +365,11 @@
   33.13                     (case apsns of
   33.14                        [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
   33.15                      | p::_ => EVERY [lift_tac Ts t p,
   33.16 -                                     rtac reflexive_thm (i+1),
   33.17 +                                     resolve_tac [reflexive_thm] (i+1),
   33.18                                       lift_split_tac] state)
   33.19              end
   33.20    in COND (has_fewer_prems i) no_tac
   33.21 -          (rtac meta_iffD i THEN lift_split_tac)
   33.22 +          (resolve_tac [meta_iffD] i THEN lift_split_tac)
   33.23    end;
   33.24  
   33.25  in (split_tac, exported_split_posns) end;  (* mk_case_split_tac *)
   33.26 @@ -400,16 +400,16 @@
   33.27        (* does not work properly if the split variable is bound by a quantifier *)
   33.28                fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
   33.29                             (if first_prem_is_disj t
   33.30 -                            then EVERY[etac Data.disjE i,rotate_tac ~1 i,
   33.31 +                            then EVERY[eresolve_tac [Data.disjE] i, rotate_tac ~1 i,
   33.32                                         rotate_tac ~1  (i+1),
   33.33                                         flat_prems_tac (i+1)]
   33.34                              else all_tac)
   33.35                             THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
   33.36                             THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
   33.37            in if n<0 then  no_tac  else (DETERM (EVERY'
   33.38 -                [rotate_tac n, etac Data.contrapos2,
   33.39 +                [rotate_tac n, eresolve_tac [Data.contrapos2],
   33.40                   split_tac splits,
   33.41 -                 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
   33.42 +                 rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1,
   33.43                   flat_prems_tac] i))
   33.44            end;
   33.45    in SUBGOAL tac
    34.1 --- a/src/Provers/trancl.ML	Thu Oct 30 21:02:01 2014 +0100
    34.2 +++ b/src/Provers/trancl.ML	Thu Oct 30 23:14:11 2014 +0100
    34.3 @@ -545,7 +545,7 @@
    34.4      let
    34.5        val SOME (_, _, rel', _) = decomp (term_of concl);
    34.6        val thms = map (prove thy rel' prems) prfs
    34.7 -    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
    34.8 +    in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
    34.9   end
   34.10   handle Cannot => Seq.empty);
   34.11  
   34.12 @@ -564,7 +564,7 @@
   34.13      let
   34.14        val SOME (_, _, rel', _) = decomp (term_of concl);
   34.15        val thms = map (prove thy rel' prems) prfs
   34.16 -    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
   34.17 +    in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
   34.18   end
   34.19   handle Cannot => Seq.empty | General.Subscript => Seq.empty);
   34.20  
    35.1 --- a/src/Pure/Isar/class.ML	Thu Oct 30 21:02:01 2014 +0100
    35.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 30 23:14:11 2014 +0100
    35.3 @@ -434,7 +434,7 @@
    35.4          (fst o rules thy) sub];
    35.5      val classrel =
    35.6        Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
    35.7 -        (K (EVERY (map (TRYALL o rtac) intros)));
    35.8 +        (K (EVERY (map (TRYALL o resolve_tac o single) intros)));
    35.9      val diff_sort = Sign.complete_sort thy [sup]
   35.10        |> subtract (op =) (Sign.complete_sort thy [sub])
   35.11        |> filter (is_class thy);
    36.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Oct 30 21:02:01 2014 +0100
    36.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Oct 30 23:14:11 2014 +0100
    36.3 @@ -56,7 +56,7 @@
    36.4          val loc_intro_tac =
    36.5            (case Locale.intros_of thy class of
    36.6              (_, NONE) => all_tac
    36.7 -          | (_, SOME intro) => ALLGOALS (rtac intro));
    36.8 +          | (_, SOME intro) => ALLGOALS (resolve_tac [intro]));
    36.9          val tac = loc_intro_tac
   36.10            THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
   36.11        in Element.prove_witness empty_ctxt prop tac end) some_prop;
    37.1 --- a/src/Pure/Isar/element.ML	Thu Oct 30 21:02:01 2014 +0100
    37.2 +++ b/src/Pure/Isar/element.ML	Thu Oct 30 23:14:11 2014 +0100
    37.3 @@ -258,14 +258,15 @@
    37.4  fun prove_witness ctxt t tac =
    37.5    Witness (t,
    37.6      Thm.close_derivation
    37.7 -      (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
    37.8 +      (Goal.prove ctxt [] [] (mark_witness t)
    37.9 +        (fn _ => resolve_tac [Drule.protectI] 1 THEN tac)));
   37.10  
   37.11  
   37.12  local
   37.13  
   37.14  val refine_witness =
   37.15    Proof.refine (Method.Basic (K (NO_CASES o
   37.16 -    K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI)))))))));
   37.17 +    K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac [Drule.protectI])))))))));
   37.18  
   37.19  fun gen_witness_proof proof after_qed wit_propss eq_props =
   37.20    let
    38.1 --- a/src/Pure/Isar/method.ML	Thu Oct 30 21:02:01 2014 +0100
    38.2 +++ b/src/Pure/Isar/method.ML	Thu Oct 30 23:14:11 2014 +0100
    38.3 @@ -100,7 +100,7 @@
    38.4  local
    38.5  
    38.6  fun cut_rule_tac rule =
    38.7 -  rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
    38.8 +  resolve_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
    38.9  
   38.10  in
   38.11  
   38.12 @@ -147,7 +147,7 @@
   38.13  
   38.14  (* this -- resolve facts directly *)
   38.15  
   38.16 -val this = METHOD (EVERY o map (HEADGOAL o rtac));
   38.17 +val this = METHOD (EVERY o map (HEADGOAL o resolve_tac o single));
   38.18  
   38.19  
   38.20  (* fact -- composition by facts from context *)
   38.21 @@ -162,7 +162,7 @@
   38.22  
   38.23  fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
   38.24    if cond (Logic.strip_assums_concl prop)
   38.25 -  then rtac rule i else no_tac);
   38.26 +  then resolve_tac [rule] i else no_tac);
   38.27  
   38.28  in
   38.29  
    39.1 --- a/src/Pure/Isar/proof.ML	Thu Oct 30 21:02:01 2014 +0100
    39.2 +++ b/src/Pure/Isar/proof.ML	Thu Oct 30 23:14:11 2014 +0100
    39.3 @@ -442,12 +442,12 @@
    39.4        Goal.norm_hhf_tac ctxt THEN'
    39.5        SUBGOAL (fn (goal, i) =>
    39.6          if can Logic.unprotect (Logic.strip_assums_concl goal) then
    39.7 -          etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
    39.8 +          eresolve_tac [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
    39.9          else finish_tac ctxt (n - 1) (i + 1));
   39.10  
   39.11  fun goal_tac ctxt rule =
   39.12    Goal.norm_hhf_tac ctxt THEN'
   39.13 -  rtac rule THEN'
   39.14 +  resolve_tac [rule] THEN'
   39.15    finish_tac ctxt (Thm.nprems_of rule);
   39.16  
   39.17  fun FINDGOAL tac st =
   39.18 @@ -886,7 +886,7 @@
   39.19  fun refine_terms n =
   39.20    refine (Method.Basic (K (NO_CASES o
   39.21      K (HEADGOAL (PRECISE_CONJUNCTS n
   39.22 -      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))
   39.23 +      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac [Drule.termI])))))))))
   39.24    #> Seq.hd;
   39.25  
   39.26  in
    40.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Oct 30 21:02:01 2014 +0100
    40.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 30 23:14:11 2014 +0100
    40.3 @@ -206,9 +206,10 @@
    40.4      val goal' = Thm.transfer thy' goal;
    40.5  
    40.6      fun limited_etac thm i =
    40.7 -      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o etac thm i;
    40.8 +      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
    40.9 +        eresolve_tac [thm] i;
   40.10      fun try_thm thm =
   40.11 -      if Thm.no_prems thm then rtac thm 1 goal'
   40.12 +      if Thm.no_prems thm then resolve_tac [thm] 1 goal'
   40.13        else
   40.14          (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
   40.15            1 goal';
    41.1 --- a/src/Pure/goal.ML	Thu Oct 30 21:02:01 2014 +0100
    41.2 +++ b/src/Pure/goal.ML	Thu Oct 30 23:14:11 2014 +0100
    41.3 @@ -293,7 +293,7 @@
    41.4  
    41.5  val adhoc_conjunction_tac = REPEAT_ALL_NEW
    41.6    (SUBGOAL (fn (goal, i) =>
    41.7 -    if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
    41.8 +    if can Logic.dest_conjunction goal then resolve_tac [Conjunction.conjunctionI] i
    41.9      else no_tac));
   41.10  
   41.11  val conjunction_tac = SUBGOAL (fn (goal, i) =>
   41.12 @@ -317,7 +317,7 @@
   41.13  (* hhf normal form *)
   41.14  
   41.15  fun norm_hhf_tac ctxt =
   41.16 -  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   41.17 +  resolve_tac [Drule.asm_rl]  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   41.18    THEN' SUBGOAL (fn (t, i) =>
   41.19      if Drule.is_norm_hhf t then all_tac
   41.20      else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
   41.21 @@ -335,7 +335,7 @@
   41.22      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
   41.23      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
   41.24      val tacs = Rs |> map (fn R =>
   41.25 -      etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   41.26 +      eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac);
   41.27    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
   41.28  
   41.29  end;
    42.1 --- a/src/Pure/raw_simplifier.ML	Thu Oct 30 21:02:01 2014 +0100
    42.2 +++ b/src/Pure/raw_simplifier.ML	Thu Oct 30 23:14:11 2014 +0100
    42.3 @@ -148,7 +148,7 @@
    42.4   {thm: thm,         (*the rewrite rule*)
    42.5    name: string,     (*name of theorem from which rewrite rule was extracted*)
    42.6    lhs: term,        (*the left-hand side*)
    42.7 -  elhs: cterm,      (*the etac-contracted lhs*)
    42.8 +  elhs: cterm,      (*the eta-contracted lhs*)
    42.9    extra: bool,      (*extra variables outside of elhs*)
   42.10    fo: bool,         (*use first-order matching*)
   42.11    perm: bool};      (*the rewrite rule is permutative*)
    43.1 --- a/src/Pure/skip_proof.ML	Thu Oct 30 21:02:01 2014 +0100
    43.2 +++ b/src/Pure/skip_proof.ML	Thu Oct 30 23:14:11 2014 +0100
    43.3 @@ -38,6 +38,6 @@
    43.4  (* cheat_tac *)
    43.5  
    43.6  fun cheat_tac i st =
    43.7 -  rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
    43.8 +  resolve_tac [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
    43.9  
   43.10  end;
    44.1 --- a/src/Pure/tactic.ML	Thu Oct 30 21:02:01 2014 +0100
    44.2 +++ b/src/Pure/tactic.ML	Thu Oct 30 23:14:11 2014 +0100
    44.3 @@ -181,7 +181,7 @@
    44.4  
    44.5  (*The conclusion of the rule gets assumed in subgoal i,
    44.6    while subgoal i+1,... are the premises of the rule.*)
    44.7 -fun cut_tac rule i = rtac cut_rl i THEN rtac rule (i + 1);
    44.8 +fun cut_tac rule i = resolve_tac [cut_rl] i THEN resolve_tac [rule] (i + 1);
    44.9  
   44.10  (*"Cut" a list of rules into the goal.  Their premises will become new
   44.11    subgoals.*)
   44.12 @@ -327,7 +327,7 @@
   44.13          | Then (SOME tac) tac' = SOME(tac THEN' tac');
   44.14        fun thins H (tac,n) =
   44.15          if p H then (tac,n+1)
   44.16 -        else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   44.17 +        else (Then tac (rotate_tac n THEN' eresolve_tac [thin_rl]),0);
   44.18    in SUBGOAL(fn (subg,n) =>
   44.19         let val Hs = Logic.strip_assums_hyp subg
   44.20         in case fst(fold thins Hs (NONE,0)) of
    45.1 --- a/src/Pure/thm.ML	Thu Oct 30 21:02:01 2014 +0100
    45.2 +++ b/src/Pure/thm.ML	Thu Oct 30 23:14:11 2014 +0100
    45.3 @@ -1390,7 +1390,7 @@
    45.4  
    45.5  (*Rotates a rule's premises to the left by k, leaving the first j premises
    45.6    unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
    45.7 -  number of premises.  Useful with etac and underlies defer_tac*)
    45.8 +  number of premises.  Useful with eresolve_tac and underlies defer_tac*)
    45.9  fun permute_prems j k rl =
   45.10    let
   45.11      val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = rl;
    46.1 --- a/src/Tools/case_product.ML	Thu Oct 30 21:02:01 2014 +0100
    46.2 +++ b/src/Tools/case_product.ML	Thu Oct 30 23:14:11 2014 +0100
    46.3 @@ -70,9 +70,9 @@
    46.4      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
    46.5      val thm2' = thm2 OF p_cons2
    46.6    in
    46.7 -    rtac (thm1 OF p_cons1)
    46.8 +    resolve_tac [thm1 OF p_cons1]
    46.9       THEN' EVERY' (map (fn p =>
   46.10 -       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
   46.11 +       resolve_tac [thm2'] THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
   46.12    end
   46.13  
   46.14  fun combine ctxt thm1 thm2 =
    47.1 --- a/src/Tools/coherent.ML	Thu Oct 30 21:02:01 2014 +0100
    47.2 +++ b/src/Tools/coherent.ML	Thu Oct 30 23:14:11 2014 +0100
    47.3 @@ -215,7 +215,7 @@
    47.4  (** external interface **)
    47.5  
    47.6  fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
    47.7 -  rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
    47.8 +  resolve_tac [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
    47.9    SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
   47.10      let
   47.11        val xs =
   47.12 @@ -227,7 +227,7 @@
   47.13          valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
   47.14            (mk_dom xs) Net.empty 0 0 of
   47.15          NONE => no_tac
   47.16 -      | SOME prf => rtac (thm_of_cl_prf ctxt'' concl [] prf) 1)
   47.17 +      | SOME prf => resolve_tac [thm_of_cl_prf ctxt'' concl [] prf] 1)
   47.18      end) ctxt' 1) ctxt;
   47.19  
   47.20  val _ = Theory.setup
    48.1 --- a/src/Tools/eqsubst.ML	Thu Oct 30 21:02:01 2014 +0100
    48.2 +++ b/src/Tools/eqsubst.ML	Thu Oct 30 23:14:11 2014 +0100
    48.3 @@ -250,7 +250,7 @@
    48.4    RW_Inst.rw ctxt m rule conclthm
    48.5    |> unfix_frees cfvs
    48.6    |> Conv.fconv_rule Drule.beta_eta_conversion
    48.7 -  |> (fn r => rtac r i st);
    48.8 +  |> (fn r => resolve_tac [r] i st);
    48.9  
   48.10  (* substitute within the conclusion of goal i of gth, using a meta
   48.11  equation rule. Note that we assume rule has var indicies zero'd *)
   48.12 @@ -332,7 +332,7 @@
   48.13        |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
   48.14    in
   48.15      (* ~j because new asm starts at back, thus we subtract 1 *)
   48.16 -    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
   48.17 +    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dresolve_tac [preelimrule] i st2)
   48.18    end;
   48.19  
   48.20  
    49.1 --- a/src/Tools/induct.ML	Thu Oct 30 21:02:01 2014 +0100
    49.2 +++ b/src/Tools/induct.ML	Thu Oct 30 23:14:11 2014 +0100
    49.3 @@ -512,7 +512,7 @@
    49.4          in
    49.5            CASES (Rule_Cases.make_common (thy,
    49.6                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
    49.7 -            ((Method.insert_tac more_facts THEN' rtac rule' THEN_ALL_NEW
    49.8 +            ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
    49.9                  (if simp then TRY o trivial_tac else K all_tac)) i) st
   49.10          end)
   49.11    end;
   49.12 @@ -683,7 +683,8 @@
   49.13    in
   49.14      (case goal_concl n [] goal of
   49.15        SOME concl =>
   49.16 -        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
   49.17 +        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
   49.18 +          resolve_tac [asm_rl]) i
   49.19      | NONE => all_tac)
   49.20    end);
   49.21  
   49.22 @@ -804,7 +805,7 @@
   49.23                |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   49.24                |> Seq.maps (fn rule' =>
   49.25                  CASES (rule_cases ctxt rule' cases)
   49.26 -                  (rtac rule' i THEN
   49.27 +                  (resolve_tac [rule'] i THEN
   49.28                      PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
   49.29        end)
   49.30        THEN_ALL_NEW_CASES
   49.31 @@ -862,7 +863,7 @@
   49.32          |> Seq.maps (fn rule' =>
   49.33            CASES (Rule_Cases.make_common (thy,
   49.34                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   49.35 -            (Method.insert_tac more_facts i THEN rtac rule' i) st))
   49.36 +            (Method.insert_tac more_facts i THEN resolve_tac [rule'] i) st))
   49.37    end);
   49.38  
   49.39  end;
    50.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Oct 30 21:02:01 2014 +0100
    50.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Oct 30 23:14:11 2014 +0100
    50.3 @@ -230,7 +230,7 @@
    50.4      key_pressed = (evt: KeyEvent) =>
    50.5        {
    50.6          evt.getKeyCode match {
    50.7 -          case KeyEvent.VK_C
    50.8 +          case KeyEvent.VK_C | KeyEvent.VK_INSERT
    50.9            if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
   50.10                text_area.getSelectionCount != 0 =>
   50.11              Registers.copy(text_area, '$')
    51.1 --- a/src/ZF/Datatype_ZF.thy	Thu Oct 30 21:02:01 2014 +0100
    51.2 +++ b/src/ZF/Datatype_ZF.thy	Thu Oct 30 23:14:11 2014 +0100
    51.3 @@ -95,7 +95,7 @@
    51.4           else ();
    51.5         val goal = Logic.mk_equals (old, new)
    51.6         val thm = Goal.prove ctxt [] [] goal
    51.7 -         (fn _ => rtac @{thm iff_reflection} 1 THEN
    51.8 +         (fn _ => resolve_tac @{thms iff_reflection} 1 THEN
    51.9             simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1)
   51.10           handle ERROR msg =>
   51.11           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
    52.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Oct 30 21:02:01 2014 +0100
    52.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Oct 30 23:14:11 2014 +0100
    52.3 @@ -289,7 +289,7 @@
    52.4        (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
    52.5        (fn {context = ctxt, ...} => EVERY
    52.6          [rewrite_goals_tac ctxt [con_def],
    52.7 -         rtac case_trans 1,
    52.8 +         resolve_tac [case_trans] 1,
    52.9           REPEAT
   52.10             (resolve_tac [@{thm refl}, split_trans,
   52.11               Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]);
   52.12 @@ -330,7 +330,7 @@
   52.13              (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg))
   52.14              (*Proves a single recursor equation.*)
   52.15              (fn {context = ctxt, ...} => EVERY
   52.16 -              [rtac recursor_trans 1,
   52.17 +              [resolve_tac [recursor_trans] 1,
   52.18                 simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1,
   52.19                 IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]);
   52.20        in
    53.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Oct 30 21:02:01 2014 +0100
    53.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 30 23:14:11 2014 +0100
    53.3 @@ -189,7 +189,7 @@
    53.4    val bnd_mono =
    53.5      Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
    53.6        (fn _ => EVERY
    53.7 -        [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
    53.8 +        [resolve_tac [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
    53.9           REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
   53.10  
   53.11    val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
   53.12 @@ -218,13 +218,13 @@
   53.13      [DETERM (stac unfold 1),
   53.14       REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
   53.15       (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
   53.16 -     rtac disjIn 2,
   53.17 +     resolve_tac [disjIn] 2,
   53.18       (*Not ares_tac, since refl must be tried before equality assumptions;
   53.19         backtracking may occur if the premises have extra variables!*)
   53.20       DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
   53.21       (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
   53.22       rewrite_goals_tac ctxt con_defs,
   53.23 -     REPEAT (rtac @{thm refl} 2),
   53.24 +     REPEAT (resolve_tac @{thms refl} 2),
   53.25       (*Typechecking; this can fail*)
   53.26       if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
   53.27       else all_tac,
   53.28 @@ -332,15 +332,15 @@
   53.29             setSolver (mk_solver "minimal"
   53.30                        (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)
   53.31                                     ORELSE' assume_tac
   53.32 -                                   ORELSE' etac @{thm FalseE}));
   53.33 +                                   ORELSE' eresolve_tac @{thms FalseE}));
   53.34  
   53.35       val quant_induct =
   53.36         Goal.prove_global thy1 [] ind_prems
   53.37           (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
   53.38           (fn {context = ctxt, prems} => EVERY
   53.39             [rewrite_goals_tac ctxt part_rec_defs,
   53.40 -            rtac (@{thm impI} RS @{thm allI}) 1,
   53.41 -            DETERM (etac raw_induct 1),
   53.42 +            resolve_tac [@{thm impI} RS @{thm allI}] 1,
   53.43 +            DETERM (eresolve_tac [raw_induct] 1),
   53.44              (*Push Part inside Collect*)
   53.45              full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
   53.46              (*This CollectE and disjE separates out the introduction rules*)
   53.47 @@ -470,8 +470,8 @@
   53.48                        (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
   53.49                     THEN
   53.50                     (*unpackage and use "prem" in the corresponding place*)
   53.51 -                   REPEAT (rtac @{thm impI} 1)  THEN
   53.52 -                   rtac (rewrite_rule ctxt all_defs prem) 1  THEN
   53.53 +                   REPEAT (resolve_tac @{thms impI} 1)  THEN
   53.54 +                   resolve_tac [rewrite_rule ctxt all_defs prem] 1  THEN
   53.55                     (*prem must not be REPEATed below: could loop!*)
   53.56                     DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
   53.57                                             eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
   53.58 @@ -483,7 +483,7 @@
   53.59           Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
   53.60             mutual_induct_concl
   53.61             (fn {context = ctxt, prems} => EVERY
   53.62 -             [rtac (quant_induct RS lemma) 1,
   53.63 +             [resolve_tac [quant_induct RS lemma] 1,
   53.64                mutual_ind_tac ctxt (rev prems) (length prems)])
   53.65         else @{thm TrueI};
   53.66  
    54.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Oct 30 21:02:01 2014 +0100
    54.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Oct 30 23:14:11 2014 +0100
    54.3 @@ -176,7 +176,8 @@
    54.4      val eqn_thms =
    54.5        eqn_terms |> map (fn t =>
    54.6          Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
    54.7 -          (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
    54.8 +          (fn {context = ctxt, ...} =>
    54.9 +            EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac @{thms refl} 1]));
   54.10  
   54.11      val (eqn_thms', thy2) =
   54.12        thy1
    55.1 --- a/src/ZF/Tools/typechk.ML	Thu Oct 30 21:02:01 2014 +0100
    55.2 +++ b/src/ZF/Tools/typechk.ML	Thu Oct 30 23:14:11 2014 +0100
    55.3 @@ -99,7 +99,7 @@
    55.4  (*Instantiates variables in typing conditions.
    55.5    drawback: does not simplify conjunctions*)
    55.6  fun type_solver_tac ctxt hyps = SELECT_GOAL
    55.7 -    (DEPTH_SOLVE (etac @{thm FalseE} 1
    55.8 +    (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
    55.9                    ORELSE basic_res_tac 1
   55.10                    ORELSE (ares_tac hyps 1
   55.11                            APPEND typecheck_step_tac (tcset_of ctxt))));
    56.1 --- a/src/ZF/arith_data.ML	Thu Oct 30 21:02:01 2014 +0100
    56.2 +++ b/src/ZF/arith_data.ML	Thu Oct 30 23:14:11 2014 +0100
    56.3 @@ -51,7 +51,7 @@
    56.4  
    56.5  (*Apply the given rewrite (if present) just once*)
    56.6  fun gen_trans_tac th2 NONE      = all_tac
    56.7 -  | gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2));
    56.8 +  | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve_tac [th RS th2]);
    56.9  
   56.10  (*Use <-> or = depending on the type of t*)
   56.11  fun mk_eq_iff(t,u) =