prefer tactics with explicit context;
authorwenzelm
Sat Jul 18 20:54:56 2015 +0200 (2015-07-18)
changeset 6075402924903a6fd
parent 60753 80ca4a065a48
child 60755 cde2b5d084e6
prefer tactics with explicit context;
src/CCL/CCL.thy
src/CCL/Type.thy
src/CCL/Wfd.thy
src/CCL/ex/Stream.thy
src/CTT/CTT.thy
src/Doc/Codegen/Evaluation.thy
src/Doc/Implementation/Isar.thy
src/Doc/Implementation/Proof.thy
src/Doc/Tutorial/Protocol/Event.thy
src/FOLP/FOLP.thy
src/FOLP/IFOLP.thy
src/FOLP/classical.ML
src/FOLP/hypsubst.ML
src/FOLP/intprover.ML
src/FOLP/simp.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxExample.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Datatype_Examples/Stream_Processor.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/approximation.ML
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOL/HOLCF/Lift.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Hoare/hoare_tac.ML
src/HOL/Hoare_Parallel/Gar_Coll.thy
src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
src/HOL/Hoare_Parallel/OG_Examples.thy
src/HOL/Hoare_Parallel/OG_Tactics.thy
src/HOL/IMPP/Com.thy
src/HOL/IMPP/Hoare.thy
src/HOL/IMPP/Natural.thy
src/HOL/IOA/Solve.thy
src/HOL/Import/import_rule.ML
src/HOL/Metis_Examples/Type_Encodings.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Prolog/prolog.ML
src/HOL/SET_Protocol/Cardholder_Registration.thy
src/HOL/SET_Protocol/Event_SET.thy
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/TLA.thy
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/Word/Word.thy
src/HOL/ex/Cartouche_Examples.thy
src/HOL/ex/Iff_Oracle.thy
src/HOL/ex/Meson_Test.thy
src/Provers/Arith/assoc_fold.ML
src/Provers/Arith/cancel_numeral_factor.ML
src/Sequents/LK.thy
src/Sequents/LK0.thy
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/CCL/CCL.thy	Sat Jul 18 20:53:05 2015 +0200
     1.2 +++ b/src/CCL/CCL.thy	Sat Jul 18 20:54:56 2015 +0200
     1.3 @@ -268,7 +268,7 @@
     1.4    let
     1.5      fun mk_raw_dstnct_thm rls s =
     1.6        Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
     1.7 -        (fn {context = ctxt, ...} => rtac @{thm notI} 1 THEN eresolve_tac ctxt rls 1)
     1.8 +        (fn {context = ctxt, ...} => resolve_tac ctxt @{thms notI} 1 THEN eresolve_tac ctxt rls 1)
     1.9    in map (mk_raw_dstnct_thm caseB_lemmas)
    1.10      (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
    1.11  
     2.1 --- a/src/CCL/Type.thy	Sat Jul 18 20:53:05 2015 +0200
     2.2 +++ b/src/CCL/Type.thy	Sat Jul 18 20:54:56 2015 +0200
     2.3 @@ -398,7 +398,7 @@
     2.4  
     2.5  ML {*
     2.6  fun genIs_tac ctxt genXH gen_mono =
     2.7 -  rtac (genXH RS @{thm iffD2}) THEN'
     2.8 +  resolve_tac ctxt [genXH RS @{thm iffD2}] THEN'
     2.9    simp_tac ctxt THEN'
    2.10    TRY o fast_tac
    2.11      (ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
    2.12 @@ -436,7 +436,7 @@
    2.13  ML {*
    2.14  fun POgen_tac ctxt (rla, rlb) i =
    2.15    SELECT_GOAL (safe_tac ctxt) i THEN
    2.16 -  rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
    2.17 +  resolve_tac ctxt [rlb RS (rla RS @{thm ssubst_pair})] i THEN
    2.18    (REPEAT (resolve_tac ctxt
    2.19        (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
    2.20          (@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @
     3.1 --- a/src/CCL/Wfd.thy	Sat Jul 18 20:53:05 2015 +0200
     3.2 +++ b/src/CCL/Wfd.thy	Sat Jul 18 20:54:56 2015 +0200
     3.3 @@ -448,7 +448,7 @@
     3.4  in
     3.5  
     3.6  fun rcall_tac ctxt i =
     3.7 -  let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps [] rl i THEN atac i
     3.8 +  let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i
     3.9    in IHinst tac @{thms rcallTs} i end
    3.10    THEN eresolve_tac ctxt @{thms rcall_lemmas} i
    3.11  
    3.12 @@ -468,7 +468,7 @@
    3.13  (*** Clean up Correctness Condictions ***)
    3.14  
    3.15  fun clean_ccs_tac ctxt =
    3.16 -  let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps [] rl i THEN atac i in
    3.17 +  let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i in
    3.18      TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
    3.19        eresolve_tac ctxt ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
    3.20        hyp_subst_tac ctxt))
    3.21 @@ -525,7 +525,7 @@
    3.22    apply (rule 1 [THEN canonical])
    3.23    apply (tactic {*
    3.24      REPEAT (DEPTH_SOLVE_1 (resolve_tac @{context} (@{thms assms} @ @{thms eval_rls}) 1 ORELSE
    3.25 -      etac @{thm substitute} 1)) *})
    3.26 +      eresolve_tac @{context} @{thms substitute} 1)) *})
    3.27    done
    3.28  
    3.29  lemma fixV: "f(fix(f)) ---> c \<Longrightarrow> fix(f) ---> c"
     4.1 --- a/src/CCL/ex/Stream.thy	Sat Jul 18 20:53:05 2015 +0200
     4.2 +++ b/src/CCL/ex/Stream.thy	Sat Jul 18 20:54:56 2015 +0200
     4.3 @@ -82,7 +82,7 @@
     4.4    apply EQgen
     4.5     prefer 2
     4.6     apply blast
     4.7 -  apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1
     4.8 +  apply (tactic {* DEPTH_SOLVE (eresolve_tac @{context} [XH_to_E @{thm ListsXH}] 1
     4.9      THEN EQgen_tac @{context} [] 1) *})
    4.10    done
    4.11  
     5.1 --- a/src/CTT/CTT.thy	Sat Jul 18 20:53:05 2015 +0200
     5.2 +++ b/src/CTT/CTT.thy	Sat Jul 18 20:54:56 2015 +0200
     5.3 @@ -421,25 +421,25 @@
     5.4      The (rtac EqE i) lets them apply to equality judgements. **)
     5.5  
     5.6  fun NE_tac ctxt sp i =
     5.7 -  TRY (rtac @{thm EqE} i) THEN
     5.8 +  TRY (resolve_tac ctxt @{thms EqE} i) THEN
     5.9    Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm NE} i
    5.10  
    5.11  fun SumE_tac ctxt sp i =
    5.12 -  TRY (rtac @{thm EqE} i) THEN
    5.13 +  TRY (resolve_tac ctxt @{thms EqE} i) THEN
    5.14    Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm SumE} i
    5.15  
    5.16  fun PlusE_tac ctxt sp i =
    5.17 -  TRY (rtac @{thm EqE} i) THEN
    5.18 +  TRY (resolve_tac ctxt @{thms EqE} i) THEN
    5.19    Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm PlusE} i
    5.20  
    5.21  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
    5.22  
    5.23  (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
    5.24  fun add_mp_tac ctxt i =
    5.25 -    rtac @{thm subst_prodE} i  THEN  assume_tac ctxt i  THEN  assume_tac ctxt i
    5.26 +  resolve_tac ctxt @{thms subst_prodE} i  THEN  assume_tac ctxt i  THEN  assume_tac ctxt i
    5.27  
    5.28  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    5.29 -fun mp_tac ctxt i = etac @{thm subst_prodE} i  THEN  assume_tac ctxt i
    5.30 +fun mp_tac ctxt i = eresolve_tac ctxt @{thms subst_prodE} i  THEN  assume_tac ctxt i
    5.31  
    5.32  (*"safe" when regarded as predicate calculus rules*)
    5.33  val safe_brls = sort (make_ord lessb)
     6.1 --- a/src/Doc/Codegen/Evaluation.thy	Sat Jul 18 20:53:05 2015 +0200
     6.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sat Jul 18 20:54:56 2015 +0200
     6.3 @@ -232,7 +232,7 @@
     6.4  ML_prf 
     6.5  (*>*) \<open>val thm =
     6.6    Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
     6.7 -by (tactic \<open>ALLGOALS (rtac thm)\<close>)
     6.8 +by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
     6.9  (*>*) 
    6.10  
    6.11  text \<open>
     7.1 --- a/src/Doc/Implementation/Isar.thy	Sat Jul 18 20:53:05 2015 +0200
     7.2 +++ b/src/Doc/Implementation/Isar.thy	Sat Jul 18 20:54:56 2015 +0200
     7.3 @@ -365,7 +365,7 @@
     7.4    assume a: A and b: B
     7.5  
     7.6    have "A \<and> B"
     7.7 -    apply (tactic \<open>rtac @{thm conjI} 1\<close>)
     7.8 +    apply (tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
     7.9      using a apply (tactic \<open>resolve_tac @{context} facts 1\<close>)
    7.10      using b apply (tactic \<open>resolve_tac @{context} facts 1\<close>)
    7.11      done
    7.12 @@ -374,7 +374,7 @@
    7.13      using a and b
    7.14      ML_val \<open>@{Isar.goal}\<close>
    7.15      apply (tactic \<open>Method.insert_tac facts 1\<close>)
    7.16 -    apply (tactic \<open>(rtac @{thm conjI} THEN_ALL_NEW atac) 1\<close>)
    7.17 +    apply (tactic \<open>(resolve_tac @{context} @{thms conjI} THEN_ALL_NEW assume_tac @{context}) 1\<close>)
    7.18      done
    7.19  end
    7.20  
     8.1 --- a/src/Doc/Implementation/Proof.thy	Sat Jul 18 20:53:05 2015 +0200
     8.2 +++ b/src/Doc/Implementation/Proof.thy	Sat Jul 18 20:54:56 2015 +0200
     8.3 @@ -492,7 +492,7 @@
     8.4    ML_prf %"ML"
     8.5     \<open>val ctxt0 = @{context};
     8.6      val (([(_, x)], [B]), ctxt1) = ctxt0
     8.7 -      |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];\<close>
     8.8 +      |> Obtain.result (fn _ => eresolve_tac ctxt0 @{thms exE} 1) [@{thm ex}];\<close>
     8.9    ML_prf %"ML"
    8.10     \<open>singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};\<close>
    8.11    ML_prf %"ML"
     9.1 --- a/src/Doc/Tutorial/Protocol/Event.thy	Sat Jul 18 20:53:05 2015 +0200
     9.2 +++ b/src/Doc/Tutorial/Protocol/Event.thy	Sat Jul 18 20:54:56 2015 +0200
     9.3 @@ -261,7 +261,7 @@
     9.4  ML
     9.5  {*
     9.6  fun analz_mono_contra_tac ctxt =
     9.7 -  rtac @{thm analz_impI} THEN' 
     9.8 +  resolve_tac ctxt @{thms analz_impI} THEN' 
     9.9    REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
    9.10    THEN' mp_tac ctxt
    9.11  *}
    9.12 @@ -331,7 +331,7 @@
    9.13  
    9.14  
    9.15  fun synth_analz_mono_contra_tac ctxt = 
    9.16 -  rtac @{thm syan_impI} THEN'
    9.17 +  resolve_tac ctxt @{thms syan_impI} THEN'
    9.18    REPEAT1 o 
    9.19      (dresolve_tac ctxt
    9.20       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    10.1 --- a/src/FOLP/FOLP.thy	Sat Jul 18 20:53:05 2015 +0200
    10.2 +++ b/src/FOLP/FOLP.thy	Sat Jul 18 20:54:56 2015 +0200
    10.3 @@ -56,7 +56,7 @@
    10.4      and r2: "!!y. y:Q ==> g(y):R"
    10.5    shows "?p : R"
    10.6    apply (rule excluded_middle [THEN disjE])
    10.7 -   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
    10.8 +   apply (tactic {* DEPTH_SOLVE (assume_tac @{context} 1 ORELSE
    10.9         resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})
   10.10    done
   10.11  
   10.12 @@ -80,8 +80,9 @@
   10.13    apply (insert major)
   10.14    apply (unfold iff_def)
   10.15    apply (rule conjE)
   10.16 -  apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE
   10.17 -      eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE
   10.18 +  apply (tactic {* DEPTH_SOLVE_1 (eresolve_tac @{context} @{thms impCE} 1 ORELSE
   10.19 +      eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN assume_tac @{context} 1 ORELSE
   10.20 +      assume_tac @{context} 1 ORELSE
   10.21        resolve_tac @{context} [@{thm r1}, @{thm r2}] 1) *})+
   10.22    done
   10.23  
   10.24 @@ -107,7 +108,7 @@
   10.25    val mp = @{thm mp}
   10.26    val not_elim = @{thm notE}
   10.27    val swap = @{thm swap}
   10.28 -  val hyp_subst_tacs = [hyp_subst_tac]
   10.29 +  fun hyp_subst_tacs ctxt = [hyp_subst_tac ctxt]
   10.30  );
   10.31  open Cla;
   10.32  
    11.1 --- a/src/FOLP/IFOLP.thy	Sat Jul 18 20:53:05 2015 +0200
    11.2 +++ b/src/FOLP/IFOLP.thy	Sat Jul 18 20:54:56 2015 +0200
    11.3 @@ -504,19 +504,19 @@
    11.4  schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
    11.5    apply (rule iffI)
    11.6     apply (tactic {*
    11.7 -     DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
    11.8 +     DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
    11.9    done
   11.10  
   11.11  schematic_lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
   11.12    apply (rule iffI)
   11.13     apply (tactic {*
   11.14 -     DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
   11.15 +     DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
   11.16    done
   11.17  
   11.18  schematic_lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
   11.19    apply (rule iffI)
   11.20     apply (tactic {*
   11.21 -     DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
   11.22 +     DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
   11.23    done
   11.24  
   11.25  lemmas pred_congs = pred1_cong pred2_cong pred3_cong
   11.26 @@ -543,7 +543,7 @@
   11.27    assumes major: "p:(P|Q)-->S"
   11.28      and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
   11.29    shows "?p:R"
   11.30 -  apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
   11.31 +  apply (tactic {* DEPTH_SOLVE (assume_tac @{context} 1 ORELSE
   11.32        resolve_tac @{context} [@{thm disjI1}, @{thm disjI2}, @{thm impI},
   11.33          @{thm major} RS @{thm mp}, @{thm minor}] 1) *})
   11.34    done
    12.1 --- a/src/FOLP/classical.ML	Sat Jul 18 20:53:05 2015 +0200
    12.2 +++ b/src/FOLP/classical.ML	Sat Jul 18 20:54:56 2015 +0200
    12.3 @@ -22,7 +22,7 @@
    12.4    val not_elim: thm             (* [| ~P;  P |] ==> R *)
    12.5    val swap: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
    12.6    val sizef : thm -> int        (* size function for BEST_FIRST *)
    12.7 -  val hyp_subst_tacs: (int -> tactic) list
    12.8 +  val hyp_subst_tacs: Proof.context -> (int -> tactic) list
    12.9    end;
   12.10  
   12.11  (*Higher precedence than := facilitates use of references*)
   12.12 @@ -70,7 +70,7 @@
   12.13  val imp_elim = make_elim mp;
   12.14  
   12.15  (*Solve goal that assumes both P and ~P. *)
   12.16 -fun contr_tac ctxt = etac not_elim THEN'  assume_tac ctxt;
   12.17 +fun contr_tac ctxt = eresolve_tac ctxt [not_elim] THEN'  assume_tac ctxt;
   12.18  
   12.19  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   12.20  fun mp_tac ctxt i = eresolve_tac ctxt ([not_elim,imp_elim]) i  THEN  assume_tac ctxt i;
   12.21 @@ -84,7 +84,7 @@
   12.22  (*Uses introduction rules in the normal way, or on negated assumptions,
   12.23    trying rules in order. *)
   12.24  fun swap_res_tac ctxt rls = 
   12.25 -    let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
   12.26 +    let fun tacf rl = resolve_tac ctxt [rl] ORELSE' eresolve_tac ctxt [rl RSN (2, swap)]
   12.27      in  assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls)
   12.28      end;
   12.29  
   12.30 @@ -152,7 +152,7 @@
   12.31    FIRST' [uniq_assume_tac ctxt,
   12.32            uniq_mp_tac ctxt,
   12.33            biresolve_tac ctxt safe0_brls,
   12.34 -          FIRST' hyp_subst_tacs,
   12.35 +          FIRST' (hyp_subst_tacs ctxt),
   12.36            biresolve_tac ctxt safep_brls] ;
   12.37  
   12.38  (*Repeatedly attack subgoals using safe inferences*)
    13.1 --- a/src/FOLP/hypsubst.ML	Sat Jul 18 20:53:05 2015 +0200
    13.2 +++ b/src/FOLP/hypsubst.ML	Sat Jul 18 20:54:56 2015 +0200
    13.3 @@ -19,8 +19,8 @@
    13.4  
    13.5  signature HYPSUBST =
    13.6    sig
    13.7 -  val bound_hyp_subst_tac : int -> tactic
    13.8 -  val hyp_subst_tac       : int -> tactic
    13.9 +  val bound_hyp_subst_tac : Proof.context -> int -> tactic
   13.10 +  val hyp_subst_tac       : Proof.context -> int -> tactic
   13.11      (*exported purely for debugging purposes*)
   13.12    val eq_var              : bool -> term -> int * thm
   13.13    val inspect_pair        : bool -> term * term -> thm
   13.14 @@ -68,16 +68,16 @@
   13.15  
   13.16  (*Select a suitable equality assumption and substitute throughout the subgoal
   13.17    Replaces only Bound variables if bnd is true*)
   13.18 -fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
   13.19 +fun gen_hyp_subst_tac bnd ctxt = SUBGOAL(fn (Bi,i) =>
   13.20        let val n = length(Logic.strip_assums_hyp Bi) - 1
   13.21            val (k,symopt) = eq_var bnd Bi
   13.22        in
   13.23           DETERM
   13.24 -           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
   13.25 -                   etac revcut_rl i,
   13.26 -                   REPEAT_DETERM_N (n-k) (etac rev_mp i),
   13.27 -                   etac (symopt RS subst) i,
   13.28 -                   REPEAT_DETERM_N n (rtac imp_intr i)])
   13.29 +           (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [rev_mp] i),
   13.30 +                   eresolve_tac ctxt [revcut_rl] i,
   13.31 +                   REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [rev_mp] i),
   13.32 +                   eresolve_tac ctxt [symopt RS subst] i,
   13.33 +                   REPEAT_DETERM_N n (resolve_tac ctxt [imp_intr] i)])
   13.34        end
   13.35        handle THM _ => no_tac | EQ_VAR => no_tac);
   13.36  
    14.1 --- a/src/FOLP/intprover.ML	Sat Jul 18 20:53:05 2015 +0200
    14.2 +++ b/src/FOLP/intprover.ML	Sat Jul 18 20:54:56 2015 +0200
    14.3 @@ -55,7 +55,7 @@
    14.4  fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt,
    14.5                              int_uniq_mp_tac ctxt,
    14.6                              biresolve_tac ctxt safe0_brls,
    14.7 -                            hyp_subst_tac,
    14.8 +                            hyp_subst_tac ctxt,
    14.9                              biresolve_tac ctxt safep_brls] ;
   14.10  
   14.11  (*Repeatedly attack subgoals using safe inferences*)
    15.1 --- a/src/FOLP/simp.ML	Sat Jul 18 20:53:05 2015 +0200
    15.2 +++ b/src/FOLP/simp.ML	Sat Jul 18 20:54:56 2015 +0200
    15.3 @@ -39,7 +39,7 @@
    15.4    val setauto   : simpset * (int -> tactic) -> simpset
    15.5    val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic
    15.6    val ASM_SIMP_TAC      : Proof.context -> simpset -> int -> tactic
    15.7 -  val CASE_TAC          : simpset -> int -> tactic
    15.8 +  val CASE_TAC          : Proof.context -> simpset -> int -> tactic
    15.9    val SIMP_CASE2_TAC    : Proof.context -> simpset -> int -> tactic
   15.10    val SIMP_THM          : Proof.context -> simpset -> thm -> thm
   15.11    val SIMP_TAC          : Proof.context -> simpset -> int -> tactic
   15.12 @@ -228,7 +228,7 @@
   15.13        in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end
   15.14    in normed end;
   15.15  
   15.16 -fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
   15.17 +fun NORM ctxt norm_lhs_tac = EVERY' [resolve_tac ctxt [red2], norm_lhs_tac, refl_tac];
   15.18  
   15.19  val trans_norms = map mk_trans normE_thms;
   15.20  
   15.21 @@ -331,9 +331,9 @@
   15.22            | find_if(_) = false;
   15.23      in find_if(tm,0) end;
   15.24  
   15.25 -fun IF1_TAC cong_tac i =
   15.26 +fun IF1_TAC ctxt cong_tac i =
   15.27      let fun seq_try (ifth::ifths,ifc::ifcs) thm =
   15.28 -                (COND (if_rewritable ifc i) (DETERM(rtac ifth i))
   15.29 +                (COND (if_rewritable ifc i) (DETERM(resolve_tac ctxt [ifth] i))
   15.30                          (seq_try(ifths,ifcs))) thm
   15.31                | seq_try([],_) thm = no_tac thm
   15.32          and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
   15.33 @@ -346,9 +346,9 @@
   15.34                  in (cong_tac THEN loop) thm end
   15.35      in COND (may_match(case_consts,i)) try_rew no_tac end;
   15.36  
   15.37 -fun CASE_TAC (SS{cong_net,...}) i =
   15.38 +fun CASE_TAC ctxt (SS{cong_net,...}) i =
   15.39  let val cong_tac = net_tac cong_net i
   15.40 -in NORM (IF1_TAC cong_tac) i end;
   15.41 +in NORM ctxt (IF1_TAC ctxt cong_tac) i end;
   15.42  
   15.43  (* Rewriting Automaton *)
   15.44  
   15.45 @@ -441,7 +441,7 @@
   15.46                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
   15.47              end
   15.48      | NONE => if more
   15.49 -            then rew((lhs_net_tac anet i THEN atac i) thm,
   15.50 +            then rew((lhs_net_tac anet i THEN assume_tac ctxt i) thm,
   15.51                       thm,ss,anet,ats,cs,false)
   15.52              else (ss,thm,anet,ats,cs);
   15.53  
   15.54 @@ -457,7 +457,7 @@
   15.55                end;
   15.56  
   15.57  fun if_exp(thm,ss,anet,ats,cs) =
   15.58 -        case Seq.pull (IF1_TAC (cong_tac i) i thm) of
   15.59 +        case Seq.pull (IF1_TAC ctxt (cong_tac i) i thm) of
   15.60                  SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
   15.61                | NONE => (ss,thm,anet,ats,cs);
   15.62  
    16.1 --- a/src/HOL/Auth/Event.thy	Sat Jul 18 20:53:05 2015 +0200
    16.2 +++ b/src/HOL/Auth/Event.thy	Sat Jul 18 20:54:56 2015 +0200
    16.3 @@ -271,7 +271,7 @@
    16.4  ML
    16.5  {*
    16.6  fun analz_mono_contra_tac ctxt = 
    16.7 -  rtac @{thm analz_impI} THEN' 
    16.8 +  resolve_tac ctxt @{thms analz_impI} THEN' 
    16.9    REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
   16.10    THEN' (mp_tac ctxt)
   16.11  *}
   16.12 @@ -287,7 +287,7 @@
   16.13  ML
   16.14  {*
   16.15  fun synth_analz_mono_contra_tac ctxt = 
   16.16 -  rtac @{thm syan_impI} THEN'
   16.17 +  resolve_tac ctxt @{thms syan_impI} THEN'
   16.18    REPEAT1 o 
   16.19      (dresolve_tac ctxt
   16.20       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    17.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Sat Jul 18 20:53:05 2015 +0200
    17.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Sat Jul 18 20:54:56 2015 +0200
    17.3 @@ -250,7 +250,7 @@
    17.4      Scan.succeed (fn ctxt =>
    17.5       (SIMPLE_METHOD
    17.6        (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
    17.7 -          REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
    17.8 +          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshCryptK_lemma}),
    17.9            ALLGOALS (asm_simp_tac
   17.10              (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))]))) *}
   17.11    "for proving useful rewrite rule"
    18.1 --- a/src/HOL/Auth/Public.thy	Sat Jul 18 20:53:05 2015 +0200
    18.2 +++ b/src/HOL/Auth/Public.thy	Sat Jul 18 20:54:56 2015 +0200
    18.3 @@ -434,7 +434,7 @@
    18.4      Scan.succeed (fn ctxt =>
    18.5       (SIMPLE_METHOD
    18.6        (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
    18.7 -          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    18.8 +          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
    18.9            ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))]))) *}
   18.10      "for proving the Session Key Compromise theorem"
   18.11  
    19.1 --- a/src/HOL/Auth/Shared.thy	Sat Jul 18 20:53:05 2015 +0200
    19.2 +++ b/src/HOL/Auth/Shared.thy	Sat Jul 18 20:54:56 2015 +0200
    19.3 @@ -238,7 +238,7 @@
    19.4      Scan.succeed (fn ctxt =>
    19.5       (SIMPLE_METHOD
    19.6        (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
    19.7 -          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    19.8 +          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
    19.9            ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))]))) *}
   19.10      "for proving the Session Key Compromise theorem"
   19.11  
    20.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Jul 18 20:53:05 2015 +0200
    20.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Jul 18 20:54:56 2015 +0200
    20.3 @@ -753,8 +753,8 @@
    20.4  
    20.5  fun analz_prepare_tac ctxt =
    20.6           prepare_tac ctxt THEN
    20.7 -         dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN 
    20.8 - (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN 
    20.9 +         dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 18 THEN 
   20.10 + (*SR9*) dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 19 THEN 
   20.11           REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
   20.12  
   20.13  end
   20.14 @@ -818,7 +818,7 @@
   20.15       (SIMPLE_METHOD
   20.16        (EVERY [REPEAT_FIRST
   20.17         (resolve_tac ctxt [allI, ballI, impI]),
   20.18 -        REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   20.19 +        REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
   20.20          ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
   20.21            addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy},
   20.22                      @{thm knows_Spy_Outpts_secureM_sr_Spy},
    21.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Jul 18 20:53:05 2015 +0200
    21.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Jul 18 20:54:56 2015 +0200
    21.3 @@ -762,8 +762,8 @@
    21.4  
    21.5  fun analz_prepare_tac ctxt = 
    21.6           prepare_tac ctxt THEN
    21.7 -         dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
    21.8 - (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
    21.9 +         dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 18 THEN 
   21.10 + (*SR_U9*) dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 19 THEN 
   21.11           REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
   21.12  
   21.13  end
   21.14 @@ -827,7 +827,7 @@
   21.15      Scan.succeed (fn ctxt =>
   21.16       (SIMPLE_METHOD
   21.17        (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
   21.18 -          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   21.19 +          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
   21.20            ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
   21.21                addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
   21.22                    @{thm knows_Spy_Outpts_secureM_srb_Spy},
    22.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 18 20:53:05 2015 +0200
    22.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 18 20:54:56 2015 +0200
    22.3 @@ -404,7 +404,7 @@
    22.4      Scan.succeed (fn ctxt =>
    22.5       (SIMPLE_METHOD
    22.6        (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
    22.7 -          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    22.8 +          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
    22.9            ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))]))) *}
   22.10      "for proving the Session Key Compromise theorem"
   22.11  
    23.1 --- a/src/HOL/Bali/AxCompl.thy	Sat Jul 18 20:53:05 2015 +0200
    23.2 +++ b/src/HOL/Bali/AxCompl.thy	Sat Jul 18 20:54:56 2015 +0200
    23.3 @@ -1370,7 +1370,7 @@
    23.4  apply -
    23.5  apply (induct_tac "n")
    23.6  apply  (tactic "ALLGOALS (clarsimp_tac @{context})")
    23.7 -apply  (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *})
    23.8 +apply  (tactic {* dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1 *})
    23.9  apply    simp
   23.10  apply   (erule finite_imageI)
   23.11  apply  (simp add: MGF_asm ax_derivs_asm)
    24.1 --- a/src/HOL/Bali/AxExample.thy	Sat Jul 18 20:53:05 2015 +0200
    24.2 +++ b/src/HOL/Bali/AxExample.thy	Sat Jul 18 20:54:56 2015 +0200
    24.3 @@ -47,7 +47,7 @@
    24.4    | NONE => Seq.empty);
    24.5  
    24.6  fun ax_tac ctxt =
    24.7 -  REPEAT o rtac allI THEN'
    24.8 +  REPEAT o resolve_tac ctxt [allI] THEN'
    24.9    resolve_tac ctxt
   24.10      @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)};
   24.11  *}
    25.1 --- a/src/HOL/Bali/AxSem.thy	Sat Jul 18 20:53:05 2015 +0200
    25.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Jul 18 20:54:56 2015 +0200
    25.3 @@ -692,8 +692,9 @@
    25.4  apply (erule ax_derivs.induct)
    25.5  (*42 subgoals*)
    25.6  apply       (tactic "ALLGOALS (strip_tac @{context})")
    25.7 -apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
    25.8 -         etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
    25.9 +apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dresolve_tac @{context} @{thms subset_singletonD},
   25.10 +         eresolve_tac @{context} [disjE],
   25.11 +         fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
   25.12  apply       (tactic "TRYALL (hyp_subst_tac @{context})")
   25.13  apply       (simp, rule ax_derivs.empty)
   25.14  apply      (drule subset_insertD)
    26.1 --- a/src/HOL/Bali/Evaln.thy	Sat Jul 18 20:53:05 2015 +0200
    26.2 +++ b/src/HOL/Bali/Evaln.thy	Sat Jul 18 20:54:56 2015 +0200
    26.3 @@ -448,9 +448,10 @@
    26.4  lemma evaln_nonstrict [rule_format (no_asm), elim]: 
    26.5    "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
    26.6  apply (erule evaln.induct)
    26.7 -apply (tactic {* ALLGOALS (EVERY' [strip_tac @{context}, TRY o etac @{thm Suc_le_D_lemma},
    26.8 +apply (tactic {* ALLGOALS (EVERY' [strip_tac @{context},
    26.9 +  TRY o eresolve_tac @{context} @{thms Suc_le_D_lemma},
   26.10    REPEAT o smp_tac @{context} 1, 
   26.11 -  resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
   26.12 +  resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW TRY o assume_tac @{context}]) *})
   26.13  (* 3 subgoals *)
   26.14  apply (auto split del: split_if)
   26.15  done
    27.1 --- a/src/HOL/Bali/TypeRel.thy	Sat Jul 18 20:53:05 2015 +0200
    27.2 +++ b/src/HOL/Bali/TypeRel.thy	Sat Jul 18 20:54:56 2015 +0200
    27.3 @@ -535,7 +535,7 @@
    27.4  apply      safe
    27.5  apply            (rule widen.int_obj)
    27.6  prefer          6 apply (drule implmt_is_class) apply simp
    27.7 -apply (tactic "ALLGOALS (etac thin_rl)")
    27.8 +apply (erule_tac [!] thin_rl)
    27.9  prefer         6 apply simp
   27.10  apply          (rule_tac [9] widen.arr_obj)
   27.11  apply         (rotate_tac [9] -1)
    28.1 --- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Sat Jul 18 20:53:05 2015 +0200
    28.2 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Sat Jul 18 20:54:56 2015 +0200
    28.3 @@ -128,16 +128,27 @@
    28.4    "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
    28.5    rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
    28.6  by (tactic {*
    28.7 -  let val ks = 1 upto 2;
    28.8 +  let
    28.9 +    val ks = 1 upto 2;
   28.10 +    val ctxt = @{context};
   28.11    in
   28.12 -    BNF_Tactics.unfold_thms_tac @{context}
   28.13 +    BNF_Tactics.unfold_thms_tac ctxt
   28.14        @{thms sp\<^sub>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.rel_Grp vimage2p_Grp} THEN
   28.15 -    HEADGOAL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
   28.16 -      BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac,
   28.17 -      rtac @{thm conversepI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
   28.18 -      BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks,
   28.19 -      REPEAT_DETERM o eresolve_tac @{context} @{thms relcomppE conversepE GrpE},
   28.20 -      hyp_subst_tac @{context}, atac])
   28.21 +    HEADGOAL (EVERY' [resolve_tac ctxt [iffI],
   28.22 +      resolve_tac ctxt @{thms relcomppI},
   28.23 +      resolve_tac ctxt @{thms GrpI},
   28.24 +      resolve_tac ctxt [refl],
   28.25 +      resolve_tac ctxt [CollectI],
   28.26 +      BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
   28.27 +      resolve_tac ctxt @{thms relcomppI}, assume_tac ctxt,
   28.28 +      resolve_tac ctxt @{thms conversepI},
   28.29 +      resolve_tac ctxt @{thms GrpI},
   28.30 +      resolve_tac ctxt [refl],
   28.31 +      resolve_tac ctxt [CollectI],
   28.32 +      BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
   28.33 +      REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
   28.34 +      hyp_subst_tac ctxt,
   28.35 +      assume_tac ctxt])
   28.36    end
   28.37  *})
   28.38  
    29.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Jul 18 20:53:05 2015 +0200
    29.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Jul 18 20:54:56 2015 +0200
    29.3 @@ -4102,7 +4102,7 @@
    29.4    THEN' CSUBGOAL (fn (g, i) =>
    29.5      let
    29.6        val th = frpar_oracle (ctxt, alternative, T, ps, g);
    29.7 -    in rtac (th RS iffD2) i end);
    29.8 +    in resolve_tac ctxt [th RS iffD2] i end);
    29.9  
   29.10  fun method alternative =
   29.11    let
    30.1 --- a/src/HOL/Decision_Procs/approximation.ML	Sat Jul 18 20:53:05 2015 +0200
    30.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Sat Jul 18 20:54:56 2015 +0200
    30.3 @@ -12,7 +12,7 @@
    30.4  structure Approximation: APPROXIMATION =
    30.5  struct
    30.6  
    30.7 -fun reorder_bounds_tac prems i =
    30.8 +fun reorder_bounds_tac ctxt prems i =
    30.9    let
   30.10      fun variable_of_bound (Const (@{const_name Trueprop}, _) $
   30.11                             (Const (@{const_name Set.member}, _) $
   30.12 @@ -35,8 +35,8 @@
   30.13                  |> Graph.strong_conn |> map the_single |> rev
   30.14                  |> map_filter (AList.lookup (op =) variable_bounds)
   30.15  
   30.16 -    fun prepend_prem th tac
   30.17 -      = tac THEN rtac (th RSN (2, @{thm mp})) i
   30.18 +    fun prepend_prem th tac =
   30.19 +      tac THEN resolve_tac ctxt [th RSN (2, @{thm mp})] i
   30.20    in
   30.21      fold prepend_prem order all_tac
   30.22    end
   30.23 @@ -49,9 +49,10 @@
   30.24    |> Thm.prop_of |> Logic.dest_equals |> snd;
   30.25  
   30.26  (* Should be in HOL.thy ? *)
   30.27 -fun gen_eval_tac conv ctxt = CONVERSION
   30.28 -  (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
   30.29 -  THEN' rtac TrueI
   30.30 +fun gen_eval_tac conv ctxt =
   30.31 +  CONVERSION
   30.32 +    (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
   30.33 +  THEN' resolve_tac ctxt [TrueI]
   30.34  
   30.35  val form_equations = @{thms interpret_form_equations};
   30.36  
   30.37 @@ -78,10 +79,10 @@
   30.38                 |> HOLogic.mk_list @{typ nat}
   30.39                 |> Thm.cterm_of ctxt
   30.40       in
   30.41 -       (rtac (Thm.instantiate ([], [((("n", 0), @{typ nat}), n),
   30.42 +       (resolve_tac ctxt [Thm.instantiate ([], [((("n", 0), @{typ nat}), n),
   30.43                                     ((("prec", 0), @{typ nat}), p),
   30.44                                     ((("ss", 0), @{typ "nat list"}), s)])
   30.45 -            @{thm "approx_form"}) i
   30.46 +            @{thm approx_form}] i
   30.47          THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
   30.48       end
   30.49  
   30.50 @@ -95,10 +96,10 @@
   30.51         val s = vs |> map lookup_splitting |> hd
   30.52              |> Thm.cterm_of ctxt
   30.53       in
   30.54 -       rtac (Thm.instantiate ([], [((("s", 0), @{typ nat}), s),
   30.55 +       resolve_tac ctxt [Thm.instantiate ([], [((("s", 0), @{typ nat}), s),
   30.56                                     ((("t", 0), @{typ nat}), t),
   30.57                                     ((("prec", 0), @{typ nat}), p)])
   30.58 -            @{thm "approx_tse_form"}) i st
   30.59 +            @{thm approx_tse_form}] i st
   30.60       end
   30.61    end
   30.62  
   30.63 @@ -190,8 +191,10 @@
   30.64    |> the |> Thm.prems_of |> hd
   30.65  
   30.66  fun prepare_form ctxt term = apply_tactic ctxt term (
   30.67 -    REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1)
   30.68 -    THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1
   30.69 +    REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
   30.70 +      eresolve_tac ctxt @{thms meta_eqE},
   30.71 +      resolve_tac ctxt @{thms impI}] 1)
   30.72 +    THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems 1) ctxt 1
   30.73      THEN DETERM (TRY (filter_prems_tac ctxt (K false) 1)))
   30.74  
   30.75  fun reify_form ctxt term = apply_tactic ctxt term
   30.76 @@ -249,10 +252,10 @@
   30.77        >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
   30.78  
   30.79  fun approximation_tac prec splitting taylor ctxt i =
   30.80 -  REPEAT (FIRST' [etac @{thm intervalE},
   30.81 -                  etac @{thm meta_eqE},
   30.82 -                  rtac @{thm impI}] i)
   30.83 -  THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
   30.84 +  REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
   30.85 +                  eresolve_tac ctxt @{thms meta_eqE},
   30.86 +                  resolve_tac ctxt @{thms impI}] i)
   30.87 +  THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i
   30.88    THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
   30.89    THEN DETERM (Reification.tac ctxt form_equations NONE i)
   30.90    THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
    31.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Jul 18 20:53:05 2015 +0200
    31.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Jul 18 20:54:56 2015 +0200
    31.3 @@ -88,9 +88,9 @@
    31.4              val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1)
    31.5            in
    31.6              ((pth RS iffD2) RS pre_thm,
    31.7 -              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    31.8 +              assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i))
    31.9            end
   31.10        | _ => (pre_thm, assm_tac i))
   31.11 -  in rtac (mp_step nh (spec_step np th)) i THEN tac end);
   31.12 +  in resolve_tac ctxt [mp_step nh (spec_step np th)] i THEN tac end);
   31.13  
   31.14  end
    32.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sat Jul 18 20:53:05 2015 +0200
    32.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sat Jul 18 20:54:56 2015 +0200
    32.3 @@ -67,9 +67,9 @@
    32.4      let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
    32.5      in 
    32.6         ((pth RS iffD2) RS pre_thm,
    32.7 -        assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    32.8 +        assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i))
    32.9      end
   32.10        | _ => (pre_thm, assm_tac i)
   32.11 -  in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
   32.12 +  in resolve_tac ctxt [(mp_step nh o spec_step np) th] i THEN tac end);
   32.13  
   32.14  end
    33.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Jul 18 20:53:05 2015 +0200
    33.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Jul 18 20:54:56 2015 +0200
    33.3 @@ -116,9 +116,9 @@
    33.4        val pth = mirfr_oracle (ctxt, Envir.eta_long [] t1)
    33.5      in 
    33.6         ((pth RS iffD2) RS pre_thm,
    33.7 -        assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    33.8 +        assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i))
    33.9      end
   33.10        | _ => (pre_thm, assm_tac i)
   33.11 -  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
   33.12 +  in resolve_tac ctxt [((mp_step nh) o (spec_step np)) th] i THEN tac end);
   33.13  
   33.14  end
    34.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Jul 18 20:53:05 2015 +0200
    34.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Jul 18 20:54:56 2015 +0200
    34.3 @@ -477,7 +477,7 @@
    34.4  apply (rule_tac x = "schA" in spec)
    34.5  apply (rule_tac x = "schB" in spec)
    34.6  apply (rule_tac x = "tr" in spec)
    34.7 -apply (tactic "thin_tac' 5 1")
    34.8 +apply (tactic "thin_tac' @{context} 5 1")
    34.9  apply (rule nat_less_induct)
   34.10  apply (rule allI)+
   34.11  apply (rename_tac tr schB schA)
   34.12 @@ -487,7 +487,7 @@
   34.13  apply (case_tac "Forall (%x. x:act B & x~:act A) tr")
   34.14  
   34.15  apply (rule seq_take_lemma [THEN iffD2, THEN spec])
   34.16 -apply (tactic "thin_tac' 5 1")
   34.17 +apply (tactic "thin_tac' @{context} 5 1")
   34.18  
   34.19  
   34.20  apply (case_tac "Finite tr")
   34.21 @@ -697,7 +697,7 @@
   34.22  apply (rule_tac x = "schA" in spec)
   34.23  apply (rule_tac x = "schB" in spec)
   34.24  apply (rule_tac x = "tr" in spec)
   34.25 -apply (tactic "thin_tac' 5 1")
   34.26 +apply (tactic "thin_tac' @{context} 5 1")
   34.27  apply (rule nat_less_induct)
   34.28  apply (rule allI)+
   34.29  apply (rename_tac tr schB schA)
   34.30 @@ -707,7 +707,7 @@
   34.31  apply (case_tac "Forall (%x. x:act A & x~:act B) tr")
   34.32  
   34.33  apply (rule seq_take_lemma [THEN iffD2, THEN spec])
   34.34 -apply (tactic "thin_tac' 5 1")
   34.35 +apply (tactic "thin_tac' @{context} 5 1")
   34.36  
   34.37  apply (case_tac "Finite tr")
   34.38  
    35.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jul 18 20:53:05 2015 +0200
    35.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jul 18 20:54:56 2015 +0200
    35.3 @@ -1098,7 +1098,7 @@
    35.4    THEN simp_tac (ctxt addsimps rws) i;
    35.5  
    35.6  fun Seq_Finite_induct_tac ctxt i =
    35.7 -  etac @{thm Seq_Finite_ind} i
    35.8 +  eresolve_tac ctxt @{thms Seq_Finite_ind} i
    35.9    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
   35.10  
   35.11  fun pair_tac ctxt s =
    36.1 --- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Jul 18 20:53:05 2015 +0200
    36.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Jul 18 20:54:56 2015 +0200
    36.3 @@ -48,9 +48,9 @@
    36.4  
    36.5  
    36.6  ML {*
    36.7 -fun thin_tac' j =
    36.8 +fun thin_tac' ctxt j =
    36.9    rotate_tac (j - 1) THEN'
   36.10 -  etac thin_rl THEN'
   36.11 +  eresolve_tac ctxt [thin_rl] THEN'
   36.12    rotate_tac (~ (j - 1))
   36.13  *}
   36.14  
   36.15 @@ -180,7 +180,7 @@
   36.16  apply (intro strip)
   36.17  apply (rule mp)
   36.18  prefer 2 apply (assumption)
   36.19 -apply (tactic "thin_tac' 1 1")
   36.20 +apply (tactic "thin_tac' @{context} 1 1")
   36.21  apply (rule_tac x = "s" in spec)
   36.22  apply (rule nat_less_induct)
   36.23  apply (intro strip)
    37.1 --- a/src/HOL/HOLCF/Lift.thy	Sat Jul 18 20:53:05 2015 +0200
    37.2 +++ b/src/HOL/HOLCF/Lift.thy	Sat Jul 18 20:54:56 2015 +0200
    37.3 @@ -46,7 +46,7 @@
    37.4  
    37.5  method_setup defined = {*
    37.6    Scan.succeed (fn ctxt => SIMPLE_METHOD'
    37.7 -    (etac @{thm lift_definedE} THEN' asm_simp_tac ctxt))
    37.8 +    (eresolve_tac ctxt @{thms lift_definedE} THEN' asm_simp_tac ctxt))
    37.9  *}
   37.10  
   37.11  lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
    38.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sat Jul 18 20:53:05 2015 +0200
    38.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sat Jul 18 20:54:56 2015 +0200
    38.3 @@ -142,7 +142,8 @@
    38.4          val cs = ContProc.cont_thms lam
    38.5          val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs
    38.6        in
    38.7 -        prove thy (def_thm::betas) goal (K [rtac reflexive_thm 1])
    38.8 +        prove thy (def_thm::betas) goal
    38.9 +          (fn {context = ctxt, ...} => [resolve_tac ctxt [reflexive_thm] 1])
   38.10        end
   38.11  end
   38.12  
   38.13 @@ -228,9 +229,9 @@
   38.14        val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
   38.15        (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
   38.16        fun tacs ctxt = [
   38.17 -          rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
   38.18 +          resolve_tac ctxt [iso_locale RS @{thm iso.casedist_rule}] 1,
   38.19            rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
   38.20 -          rtac thm3 1]
   38.21 +          resolve_tac ctxt [thm3] 1]
   38.22      in
   38.23        val nchotomy = prove thy con_betas goal (tacs o #context)
   38.24        val exhaust =
   38.25 @@ -245,8 +246,8 @@
   38.26          val rules = @{thms compact_sinl compact_sinr compact_spair
   38.27                             compact_up compact_ONE}
   38.28          fun tacs ctxt =
   38.29 -          [rtac (iso_locale RS @{thm iso.compact_abs}) 1,
   38.30 -           REPEAT (resolve_tac ctxt rules 1 ORELSE atac 1)]
   38.31 +          [resolve_tac ctxt [iso_locale RS @{thm iso.compact_abs}] 1,
   38.32 +           REPEAT (resolve_tac ctxt rules 1 ORELSE assume_tac ctxt 1)]
   38.33          fun con_compact (con, args) =
   38.34            let
   38.35              val vs = vars_of args
   38.36 @@ -709,7 +710,10 @@
   38.37      local
   38.38        fun dis_strict dis =
   38.39          let val goal = mk_trp (mk_strict dis)
   38.40 -        in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end
   38.41 +        in
   38.42 +          prove thy dis_defs goal
   38.43 +            (fn {context = ctxt, ...} => [resolve_tac ctxt [hd case_rews] 1])
   38.44 +        end
   38.45      in
   38.46        val dis_stricts = map dis_strict dis_consts
   38.47      end
   38.48 @@ -739,9 +743,9 @@
   38.49            val x = Free ("x", lhsT)
   38.50            val simps = dis_apps @ @{thms dist_eq_tr}
   38.51            fun tacs ctxt =
   38.52 -            [rtac @{thm iffI} 1,
   38.53 +            [resolve_tac ctxt @{thms iffI} 1,
   38.54               asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps dis_stricts) 2,
   38.55 -             rtac exhaust 1, atac 1,
   38.56 +             resolve_tac ctxt [exhaust] 1, assume_tac ctxt 1,
   38.57               ALLGOALS (asm_full_simp_tac (put_simpset simple_ss ctxt addsimps simps))]
   38.58            val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x))
   38.59          in prove thy [] goal (tacs o #context) end
    39.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Jul 18 20:53:05 2015 +0200
    39.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Jul 18 20:54:56 2015 +0200
    39.3 @@ -161,11 +161,11 @@
    39.4                val rules = prems @ con_rews @ @{thms simp_thms}
    39.5                val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules)
    39.6                fun arg_tac (lazy, _) =
    39.7 -                  rtac (if lazy then allI else case_UU_allI) 1
    39.8 +                  resolve_tac ctxt [if lazy then allI else case_UU_allI] 1
    39.9                fun tacs ctxt =
   39.10                    rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} ::
   39.11                    map arg_tac args @
   39.12 -                  [REPEAT (rtac impI 1), ALLGOALS simplify]
   39.13 +                  [REPEAT (resolve_tac ctxt [impI] 1), ALLGOALS simplify]
   39.14              in
   39.15                Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context)
   39.16              end
   39.17 @@ -181,7 +181,7 @@
   39.18              TRY (safe_tac (put_claset HOL_cs ctxt))]
   39.19            fun con_tac _ = 
   39.20              asm_simp_tac (put_simpset take_ss ctxt) 1 THEN
   39.21 -            (resolve_tac ctxt prems' THEN_ALL_NEW etac spec) 1
   39.22 +            (resolve_tac ctxt prems' THEN_ALL_NEW eresolve_tac ctxt [spec]) 1
   39.23            fun cases_tacs (cons, exhaust) =
   39.24              Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), "x")] [] exhaust 1 ::
   39.25              asm_simp_tac (put_simpset take_ss ctxt addsimps prems) 1 ::
   39.26 @@ -201,9 +201,9 @@
   39.27        fun tacf {prems, context = ctxt} =
   39.28          let
   39.29            fun finite_tac (take_induct, fin_ind) =
   39.30 -              rtac take_induct 1 THEN
   39.31 +              resolve_tac ctxt [take_induct] 1 THEN
   39.32                (if is_finite then all_tac else resolve_tac ctxt prems 1) THEN
   39.33 -              (rtac fin_ind THEN_ALL_NEW solve_tac ctxt prems) 1
   39.34 +              (resolve_tac ctxt [fin_ind] THEN_ALL_NEW solve_tac ctxt prems) 1
   39.35            val fin_inds = Project_Rule.projections ctxt finite_ind
   39.36          in
   39.37            TRY (safe_tac (put_claset HOL_cs ctxt)) THEN
   39.38 @@ -326,10 +326,10 @@
   39.39            val prems' = Project_Rule.projections ctxt prem'
   39.40            val dests = map (fn th => th RS spec RS spec RS mp) prems'
   39.41            fun one_tac (dest, rews) =
   39.42 -              dtac dest 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN
   39.43 +              dresolve_tac ctxt [dest] 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN
   39.44                ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rews))
   39.45          in
   39.46 -          rtac @{thm nat.induct} 1 THEN
   39.47 +          resolve_tac ctxt @{thms nat.induct} 1 THEN
   39.48            simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1 THEN
   39.49            safe_tac (put_claset HOL_cs ctxt) THEN
   39.50            EVERY (map one_tac (dests ~~ take_rews))
   39.51 @@ -350,7 +350,7 @@
   39.52          let
   39.53            val rule = hd prems RS coind_lemma
   39.54          in
   39.55 -          rtac take_lemma 1 THEN
   39.56 +          resolve_tac ctxt [take_lemma] 1 THEN
   39.57            asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (rule :: prems)) 1
   39.58          end
   39.59      in
    40.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Jul 18 20:53:05 2015 +0200
    40.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Jul 18 20:54:56 2015 +0200
    40.3 @@ -310,12 +310,12 @@
    40.4          Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
    40.5           EVERY
    40.6            [rewrite_goals_tac ctxt map_apply_thms,
    40.7 -           rtac (map_cont_thm RS @{thm cont_fix_ind}) 1,
    40.8 +           resolve_tac ctxt [map_cont_thm RS @{thm cont_fix_ind}] 1,
    40.9             REPEAT (resolve_tac ctxt adm_rules 1),
   40.10             simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
   40.11             simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
   40.12 -           REPEAT (etac @{thm conjE} 1),
   40.13 -           REPEAT (resolve_tac ctxt (deflation_rules @ prems) 1 ORELSE atac 1)])
   40.14 +           REPEAT (eresolve_tac ctxt @{thms conjE} 1),
   40.15 +           REPEAT (resolve_tac ctxt (deflation_rules @ prems) 1 ORELSE assume_tac ctxt 1)])
   40.16        end
   40.17      fun conjuncts [] _ = []
   40.18        | conjuncts (n::[]) thm = [(n, thm)]
   40.19 @@ -623,14 +623,13 @@
   40.20          Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
   40.21           EVERY
   40.22            [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),
   40.23 -           rtac (@{thm cont_parallel_fix_ind}
   40.24 -             OF [defl_cont_thm, map_cont_thm]) 1,
   40.25 +           resolve_tac ctxt [@{thm cont_parallel_fix_ind} OF [defl_cont_thm, map_cont_thm]] 1,
   40.26             REPEAT (resolve_tac ctxt adm_rules 1),
   40.27             simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
   40.28             simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
   40.29             simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1,
   40.30 -           REPEAT (etac @{thm conjE} 1),
   40.31 -           REPEAT (resolve_tac ctxt (isodefl_rules @ prems) 1 ORELSE atac 1)])
   40.32 +           REPEAT (eresolve_tac ctxt @{thms conjE} 1),
   40.33 +           REPEAT (resolve_tac ctxt (isodefl_rules @ prems) 1 ORELSE assume_tac ctxt 1)])
   40.34        end
   40.35      val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
   40.36      fun conjuncts [] _ = []
   40.37 @@ -655,9 +654,9 @@
   40.38          val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts))
   40.39          val goal = mk_eqs (lhs, mk_ID lhsT)
   40.40          fun tac ctxt = EVERY
   40.41 -          [rtac @{thm isodefl_DEFL_imp_ID} 1,
   40.42 +          [resolve_tac ctxt @{thms isodefl_DEFL_imp_ID} 1,
   40.43             stac ctxt DEFL_thm 1,
   40.44 -           rtac isodefl_thm 1,
   40.45 +           resolve_tac ctxt [isodefl_thm] 1,
   40.46             REPEAT (resolve_tac ctxt @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)]
   40.47        in
   40.48          Goal.prove_global thy [] [] goal (tac o #context)
   40.49 @@ -700,8 +699,8 @@
   40.50              EVERY
   40.51              [simp_tac (put_simpset HOL_basic_ss ctxt addsimps start_rules) 1,
   40.52               simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms fix_def2}) 1,
   40.53 -             rtac @{thm lub_eq} 1,
   40.54 -             rtac @{thm nat.induct} 1,
   40.55 +             resolve_tac ctxt @{thms lub_eq} 1,
   40.56 +             resolve_tac ctxt @{thms nat.induct} 1,
   40.57               simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules0) 1,
   40.58               asm_full_simp_tac (put_simpset beta_ss ctxt addsimps rules1) 1]
   40.59        in
   40.60 @@ -713,12 +712,13 @@
   40.61        let
   40.62          val n = Free ("n", natT)
   40.63          val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
   40.64 -        val tac =
   40.65 +        fun tac ctxt =
   40.66              EVERY
   40.67 -            [rtac @{thm trans} 1, rtac map_ID_thm 2,
   40.68 +            [resolve_tac ctxt @{thms trans} 1,
   40.69 +             resolve_tac ctxt [map_ID_thm] 2,
   40.70               cut_tac lub_take_lemma 1,
   40.71 -             REPEAT (etac @{thm Pair_inject} 1), atac 1]
   40.72 -        val lub_take_thm = Goal.prove_global thy [] [] goal (K tac)
   40.73 +             REPEAT (eresolve_tac ctxt @{thms Pair_inject} 1), assume_tac ctxt 1]
   40.74 +        val lub_take_thm = Goal.prove_global thy [] [] goal (tac o #context)
   40.75        in
   40.76          add_qualified_thm "lub_take" (dbind, lub_take_thm) thy
   40.77        end
    41.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Jul 18 20:53:05 2015 +0200
    41.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Jul 18 20:54:56 2015 +0200
    41.3 @@ -320,12 +320,12 @@
    41.4        in
    41.5          Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} =>
    41.6           EVERY
    41.7 -          [rtac @{thm nat.induct} 1,
    41.8 +          [resolve_tac ctxt @{thms nat.induct} 1,
    41.9             simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
   41.10             asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1,
   41.11 -           REPEAT (etac @{thm conjE} 1
   41.12 +           REPEAT (eresolve_tac ctxt @{thms conjE} 1
   41.13                     ORELSE resolve_tac ctxt deflation_rules 1
   41.14 -                   ORELSE atac 1)])
   41.15 +                   ORELSE assume_tac ctxt 1)])
   41.16        end
   41.17      fun conjuncts [] _ = []
   41.18        | conjuncts (n::[]) thm = [(n, thm)]
   41.19 @@ -444,7 +444,7 @@
   41.20              take_Suc_thms @ decisive_abs_rep_thms
   41.21              @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}
   41.22          fun tac ctxt = EVERY [
   41.23 -            rtac @{thm nat.induct} 1,
   41.24 +            resolve_tac ctxt @{thms nat.induct} 1,
   41.25              simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1,
   41.26              asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1]
   41.27        in Goal.prove_global thy [] [] goal (tac o #context) end
   41.28 @@ -461,7 +461,7 @@
   41.29          fun tac ctxt =
   41.30              EVERY [
   41.31              rewrite_goals_tac ctxt finite_defs,
   41.32 -            rtac @{thm lub_ID_finite} 1,
   41.33 +            resolve_tac ctxt @{thms lub_ID_finite} 1,
   41.34              resolve_tac ctxt chain_take_thms 1,
   41.35              resolve_tac ctxt lub_take_thms 1,
   41.36              resolve_tac ctxt decisive_thms 1]
    42.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Sat Jul 18 20:53:05 2015 +0200
    42.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Sat Jul 18 20:54:56 2015 +0200
    42.3 @@ -102,7 +102,7 @@
    42.4      fun new_cont_tac f' i =
    42.5        case all_cont_thms f' of
    42.6          [] => no_tac
    42.7 -      | (c::_) => rtac c i
    42.8 +      | (c::_) => resolve_tac ctxt [c] i
    42.9  
   42.10      fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
   42.11        let
    43.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Sat Jul 18 20:53:05 2015 +0200
    43.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sat Jul 18 20:54:56 2015 +0200
    43.3 @@ -73,8 +73,8 @@
    43.4      val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
    43.5      val (full_tname, Ts) = dest_Type newT
    43.6      val lhs_sorts = map (snd o dest_TFree) Ts
    43.7 -    val tac = rtac (@{thm typedef_cpo} OF cpo_thms) 1
    43.8 -    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
    43.9 +    fun tac ctxt = resolve_tac ctxt [@{thm typedef_cpo} OF cpo_thms] 1
   43.10 +    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy
   43.11      (* transfer thms so that they will know about the new cpo instance *)
   43.12      val cpo_thms' = map (Thm.transfer thy) cpo_thms
   43.13      fun make thm = Drule.zero_var_indexes (thm OF cpo_thms')
   43.14 @@ -112,8 +112,8 @@
   43.15      val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
   43.16      val (full_tname, Ts) = dest_Type newT
   43.17      val lhs_sorts = map (snd o dest_TFree) Ts
   43.18 -    val tac = rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
   43.19 -    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
   43.20 +    fun tac ctxt = resolve_tac ctxt [@{thm typedef_pcpo} OF pcpo_thms] 1
   43.21 +    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy
   43.22      val pcpo_thms' = map (Thm.transfer thy) pcpo_thms
   43.23      fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms')
   43.24      val Rep_strict = make @{thm typedef_Rep_strict}
   43.25 @@ -182,7 +182,7 @@
   43.26      val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
   43.27      val thy = lthy
   43.28        |> Class.prove_instantiation_exit
   43.29 -          (K (rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
   43.30 +          (fn ctxt => resolve_tac ctxt [@{thm typedef_po} OF [type_definition, below_def]] 1)
   43.31    in ((info, below_def), thy) end
   43.32  
   43.33  fun prepare_cpodef
   43.34 @@ -205,7 +205,7 @@
   43.35      fun cpodef_result nonempty admissible thy =
   43.36        let
   43.37          val ((info as (_, {type_definition, ...}), below_def), thy) = thy
   43.38 -          |> add_podef typ set opt_morphs (fn _ => rtac nonempty 1)
   43.39 +          |> add_podef typ set opt_morphs (fn ctxt => resolve_tac ctxt [nonempty] 1)
   43.40          val (cpo_info, thy) = thy
   43.41            |> prove_cpo name newT morphs type_definition below_def admissible
   43.42        in
   43.43 @@ -237,7 +237,7 @@
   43.44  
   43.45      fun pcpodef_result bottom_mem admissible thy =
   43.46        let
   43.47 -        fun tac _ = rtac exI 1 THEN rtac bottom_mem 1
   43.48 +        fun tac ctxt = resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt [bottom_mem] 1
   43.49          val ((info as (_, {type_definition, ...}), below_def), thy) = thy
   43.50            |> add_podef typ set opt_morphs tac
   43.51          val (cpo_info, thy) = thy
    44.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Sat Jul 18 20:53:05 2015 +0200
    44.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sat Jul 18 20:54:56 2015 +0200
    44.3 @@ -108,8 +108,8 @@
    44.4      val set = @{term "defl_set :: udom defl => udom set"} $ defl
    44.5  
    44.6      (*pcpodef*)
    44.7 -    fun tac1 _ = rtac @{thm defl_set_bottom} 1
    44.8 -    fun tac2 _ = rtac @{thm adm_defl_set} 1
    44.9 +    fun tac1 ctxt = resolve_tac ctxt @{thms defl_set_bottom} 1
   44.10 +    fun tac2 ctxt = resolve_tac ctxt @{thms adm_defl_set} 1
   44.11      val ((info, cpo_info, pcpo_info), thy) = thy
   44.12        |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2)
   44.13  
   44.14 @@ -165,7 +165,7 @@
   44.15        liftemb_def, liftprj_def, liftdefl_def]
   44.16      val thy = lthy
   44.17        |> Class.prove_instantiation_instance
   44.18 -          (K (rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
   44.19 +          (fn ctxt => resolve_tac ctxt [@{thm typedef_domain_class} OF typedef_thms] 1)
   44.20        |> Local_Theory.exit_global
   44.21  
   44.22      (*other theorems*)
    45.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Jul 18 20:53:05 2015 +0200
    45.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Jul 18 20:54:56 2015 +0200
    45.3 @@ -301,7 +301,7 @@
    45.4          val unfold_thm = the (Symtab.lookup tab c)
    45.5          val rule = unfold_thm RS @{thm ssubst_lhs}
    45.6        in
    45.7 -        CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ctxt i)
    45.8 +        CHANGED (resolve_tac ctxt [rule] i THEN eta_tac i THEN asm_simp_tac ctxt i)
    45.9        end
   45.10    in
   45.11      SUBGOAL (fn ti => the_default no_tac (try tac ti))
   45.12 @@ -311,7 +311,7 @@
   45.13  fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
   45.14    let
   45.15      val rule = unfold_thm RS @{thm ssubst_lhs}
   45.16 -    val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ctxt 1
   45.17 +    val tac = resolve_tac ctxt [rule] 1 THEN eta_tac 1 THEN asm_simp_tac ctxt 1
   45.18      fun prove_term t = Goal.prove ctxt [] [] t (K tac)
   45.19      fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t)
   45.20    in
    46.1 --- a/src/HOL/Hoare/hoare_tac.ML	Sat Jul 18 20:53:05 2015 +0200
    46.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Sat Jul 18 20:54:56 2015 +0200
    46.3 @@ -132,9 +132,9 @@
    46.4  fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
    46.5    before_set2pred_simp_tac ctxt i THEN_MAYBE
    46.6    EVERY [
    46.7 -    rtac subsetI i,
    46.8 -    rtac CollectI i,
    46.9 -    dtac CollectD i,
   46.10 +    resolve_tac ctxt [subsetI] i,
   46.11 +    resolve_tac ctxt [CollectI] i,
   46.12 +    dresolve_tac ctxt [CollectD] i,
   46.13      TRY (split_all_tac ctxt i) THEN_MAYBE
   46.14       (rename_tac var_names i THEN
   46.15        full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
   46.16 @@ -148,7 +148,8 @@
   46.17  (*******************************************************************************)
   46.18  
   46.19  fun max_simp_tac ctxt var_names tac =
   46.20 -  FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
   46.21 +  FIRST' [resolve_tac ctxt [subset_refl],
   46.22 +    set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
   46.23  
   46.24  fun basic_simp_tac ctxt var_names tac =
   46.25    simp_tac
   46.26 @@ -163,26 +164,28 @@
   46.27    let
   46.28      val var_names = map (fst o dest_Free) vars;
   46.29      fun wlp_tac i =
   46.30 -      rtac @{thm SeqRule} i THEN rule_tac false (i + 1)
   46.31 +      resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1)
   46.32      and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
   46.33        ((wlp_tac i THEN rule_tac pre_cond i)
   46.34          ORELSE
   46.35          (FIRST [
   46.36 -          rtac @{thm SkipRule} i,
   46.37 -          rtac @{thm AbortRule} i,
   46.38 +          resolve_tac ctxt @{thms SkipRule} i,
   46.39 +          resolve_tac ctxt @{thms AbortRule} i,
   46.40            EVERY [
   46.41 -            rtac @{thm BasicRule} i,
   46.42 -            rtac Mlem i,
   46.43 +            resolve_tac ctxt @{thms BasicRule} i,
   46.44 +            resolve_tac ctxt [Mlem] i,
   46.45              split_simp_tac ctxt i],
   46.46            EVERY [
   46.47 -            rtac @{thm CondRule} i,
   46.48 +            resolve_tac ctxt @{thms CondRule} i,
   46.49              rule_tac false (i + 2),
   46.50              rule_tac false (i + 1)],
   46.51            EVERY [
   46.52 -            rtac @{thm WhileRule} i,
   46.53 +            resolve_tac ctxt @{thms WhileRule} i,
   46.54              basic_simp_tac ctxt var_names tac (i + 2),
   46.55              rule_tac true (i + 1)]]
   46.56 -         THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
   46.57 +         THEN (
   46.58 +           if pre_cond then basic_simp_tac ctxt var_names tac i
   46.59 +           else resolve_tac ctxt [subset_refl] i)));
   46.60    in rule_tac end;
   46.61  
   46.62  
    47.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sat Jul 18 20:53:05 2015 +0200
    47.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sat Jul 18 20:54:56 2015 +0200
    47.3 @@ -775,11 +775,21 @@
    47.4  --\<open>20 subgoals left\<close>
    47.5  apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>)
    47.6  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    47.7 -apply(tactic \<open>TRYALL (etac disjE)\<close>)
    47.8 +apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
    47.9  apply simp_all
   47.10 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\<close>)
   47.11 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}])\<close>)
   47.12 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\<close>)
   47.13 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   47.14 +    resolve_tac @{context} [subset_trans],
   47.15 +    eresolve_tac @{context} @{thms Graph3},
   47.16 +    force_tac @{context},
   47.17 +    assume_tac @{context}])\<close>)
   47.18 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   47.19 +    eresolve_tac @{context} [subset_trans],
   47.20 +    resolve_tac @{context} @{thms Graph9},
   47.21 +    force_tac @{context}])\<close>)
   47.22 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI1],
   47.23 +    eresolve_tac @{context} @{thms psubset_subset_trans},
   47.24 +    resolve_tac @{context} @{thms Graph9},
   47.25 +    force_tac @{context}])\<close>)
   47.26  done
   47.27  
   47.28  subsubsection \<open>Interference freedom Mutator-Collector\<close>
    48.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Sat Jul 18 20:53:05 2015 +0200
    48.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Sat Jul 18 20:54:56 2015 +0200
    48.3 @@ -1178,40 +1178,62 @@
    48.4  --\<open>14 subgoals left\<close>
    48.5  apply(tactic \<open>TRYALL (clarify_tac @{context})\<close>)
    48.6  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    48.7 -apply(tactic \<open>TRYALL (rtac conjI)\<close>)
    48.8 -apply(tactic \<open>TRYALL (rtac impI)\<close>)
    48.9 -apply(tactic \<open>TRYALL (etac disjE)\<close>)
   48.10 -apply(tactic \<open>TRYALL (etac conjE)\<close>)
   48.11 -apply(tactic \<open>TRYALL (etac disjE)\<close>)
   48.12 -apply(tactic \<open>TRYALL (etac disjE)\<close>)
   48.13 +apply(tactic \<open>TRYALL (resolve_tac @{context} [conjI])\<close>)
   48.14 +apply(tactic \<open>TRYALL (resolve_tac @{context} [impI])\<close>)
   48.15 +apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
   48.16 +apply(tactic \<open>TRYALL (eresolve_tac @{context} [conjE])\<close>)
   48.17 +apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
   48.18 +apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
   48.19  --\<open>72 subgoals left\<close>
   48.20  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   48.21  --\<open>35 subgoals left\<close>
   48.22 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\<close>)
   48.23 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI1],
   48.24 +    resolve_tac @{context} [subset_trans],
   48.25 +    eresolve_tac @{context} @{thms Graph3},
   48.26 +    force_tac @{context},
   48.27 +    assume_tac @{context}])\<close>)
   48.28  --\<open>28 subgoals left\<close>
   48.29 -apply(tactic \<open>TRYALL (etac conjE)\<close>)
   48.30 -apply(tactic \<open>TRYALL (etac disjE)\<close>)
   48.31 +apply(tactic \<open>TRYALL (eresolve_tac @{context} [conjE])\<close>)
   48.32 +apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
   48.33  --\<open>34 subgoals left\<close>
   48.34  apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   48.35  apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   48.36  apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
   48.37  apply(simp_all add:Graph10)
   48.38  --\<open>47 subgoals left\<close>
   48.39 -apply(tactic \<open>TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}])\<close>)
   48.40 +apply(tactic \<open>TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2],
   48.41 +    eresolve_tac @{context} @{thms subset_psubset_trans},
   48.42 +    eresolve_tac @{context} @{thms Graph11},
   48.43 +    force_tac @{context}])\<close>)
   48.44  --\<open>41 subgoals left\<close>
   48.45 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
   48.46 -    force_tac (@{context} addsimps
   48.47 -      [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])])\<close>)
   48.48 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   48.49 +    resolve_tac @{context} [disjI1],
   48.50 +    eresolve_tac @{context} @{thms le_trans},
   48.51 +    force_tac (@{context} addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])\<close>)
   48.52  --\<open>35 subgoals left\<close>
   48.53 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\<close>)
   48.54 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   48.55 +    resolve_tac @{context} [disjI1],
   48.56 +    eresolve_tac @{context} @{thms psubset_subset_trans},
   48.57 +    resolve_tac @{context} @{thms Graph9},
   48.58 +    force_tac @{context}])\<close>)
   48.59  --\<open>31 subgoals left\<close>
   48.60 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\<close>)
   48.61 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   48.62 +    resolve_tac @{context} [disjI1],
   48.63 +    eresolve_tac @{context} @{thms subset_psubset_trans},
   48.64 +    eresolve_tac @{context} @{thms Graph11},
   48.65 +    force_tac @{context}])\<close>)
   48.66  --\<open>29 subgoals left\<close>
   48.67 -apply(tactic \<open>TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\<close>)
   48.68 +apply(tactic \<open>TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2],
   48.69 +    eresolve_tac @{context} @{thms subset_psubset_trans},
   48.70 +    eresolve_tac @{context} @{thms subset_psubset_trans},
   48.71 +    eresolve_tac @{context} @{thms Graph11},
   48.72 +    force_tac @{context}])\<close>)
   48.73  --\<open>25 subgoals left\<close>
   48.74 -apply(tactic \<open>TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
   48.75 -    force_tac (@{context} addsimps
   48.76 -      [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])])\<close>)
   48.77 +apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   48.78 +    resolve_tac @{context} [disjI2],
   48.79 +    resolve_tac @{context} [disjI1],
   48.80 +    eresolve_tac @{context} @{thms le_trans},
   48.81 +    force_tac (@{context} addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])\<close>)
   48.82  --\<open>10 subgoals left\<close>
   48.83  apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
   48.84  done
    49.1 --- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Sat Jul 18 20:53:05 2015 +0200
    49.2 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sat Jul 18 20:54:56 2015 +0200
    49.3 @@ -434,7 +434,7 @@
    49.4  --\<open>112 subgoals left\<close>
    49.5  apply(simp_all (no_asm))
    49.6  --\<open>43 subgoals left\<close>
    49.7 -apply(tactic \<open>ALLGOALS (conjI_Tac (K all_tac))\<close>)
    49.8 +apply(tactic \<open>ALLGOALS (conjI_Tac @{context} (K all_tac))\<close>)
    49.9  --\<open>419 subgoals left\<close>
   49.10  apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
   49.11  --\<open>99 subgoals left\<close>
    50.1 --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Sat Jul 18 20:53:05 2015 +0200
    50.2 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Sat Jul 18 20:54:56 2015 +0200
    50.3 @@ -291,9 +291,9 @@
    50.4  @{text n} subgoals, one for each conjunct:\<close>
    50.5  
    50.6  ML \<open>
    50.7 -fun conjI_Tac tac i st = st |>
    50.8 -       ( (EVERY [rtac conjI i,
    50.9 -          conjI_Tac tac (i+1),
   50.10 +fun conjI_Tac ctxt tac i st = st |>
   50.11 +       ( (EVERY [resolve_tac ctxt [conjI] i,
   50.12 +          conjI_Tac ctxt tac (i+1),
   50.13            tac i]) ORELSE (tac i) )
   50.14  \<close>
   50.15  
   50.16 @@ -326,119 +326,123 @@
   50.17  
   50.18  ML \<open>
   50.19  
   50.20 -fun WlpTac ctxt i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac ctxt false (i+1))
   50.21 +fun WlpTac ctxt i = resolve_tac ctxt @{thms SeqRule} i THEN HoareRuleTac ctxt false (i + 1)
   50.22  and HoareRuleTac ctxt precond i st = st |>
   50.23      ( (WlpTac ctxt i THEN HoareRuleTac ctxt precond i)
   50.24        ORELSE
   50.25 -      (FIRST[rtac (@{thm SkipRule}) i,
   50.26 -             rtac (@{thm BasicRule}) i,
   50.27 -             EVERY[rtac (@{thm ParallelConseqRule}) i,
   50.28 +      (FIRST[resolve_tac ctxt @{thms SkipRule} i,
   50.29 +             resolve_tac ctxt @{thms BasicRule} i,
   50.30 +             EVERY[resolve_tac ctxt @{thms ParallelConseqRule} i,
   50.31                     ParallelConseq ctxt (i+2),
   50.32                     ParallelTac ctxt (i+1),
   50.33                     ParallelConseq ctxt i],
   50.34 -             EVERY[rtac (@{thm CondRule}) i,
   50.35 +             EVERY[resolve_tac ctxt @{thms CondRule} i,
   50.36                     HoareRuleTac ctxt false (i+2),
   50.37                     HoareRuleTac ctxt false (i+1)],
   50.38 -             EVERY[rtac (@{thm WhileRule}) i,
   50.39 +             EVERY[resolve_tac ctxt @{thms WhileRule} i,
   50.40                     HoareRuleTac ctxt true (i+1)],
   50.41               K all_tac i ]
   50.42 -       THEN (if precond then (K all_tac i) else (rtac (@{thm subset_refl}) i))))
   50.43 +       THEN (if precond then (K all_tac i) else resolve_tac ctxt @{thms subset_refl} i)))
   50.44  
   50.45 -and AnnWlpTac ctxt i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac ctxt (i+1))
   50.46 +and AnnWlpTac ctxt i = resolve_tac ctxt @{thms AnnSeq} i THEN AnnHoareRuleTac ctxt (i + 1)
   50.47  and AnnHoareRuleTac ctxt i st = st |>
   50.48      ( (AnnWlpTac ctxt i THEN AnnHoareRuleTac ctxt i )
   50.49       ORELSE
   50.50 -      (FIRST[(rtac (@{thm AnnskipRule}) i),
   50.51 -             EVERY[rtac (@{thm AnnatomRule}) i,
   50.52 +      (FIRST[(resolve_tac ctxt @{thms AnnskipRule} i),
   50.53 +             EVERY[resolve_tac ctxt @{thms AnnatomRule} i,
   50.54                     HoareRuleTac ctxt true (i+1)],
   50.55 -             (rtac (@{thm AnnwaitRule}) i),
   50.56 -             rtac (@{thm AnnBasic}) i,
   50.57 -             EVERY[rtac (@{thm AnnCond1}) i,
   50.58 +             (resolve_tac ctxt @{thms AnnwaitRule} i),
   50.59 +             resolve_tac ctxt @{thms AnnBasic} i,
   50.60 +             EVERY[resolve_tac ctxt @{thms AnnCond1} i,
   50.61                     AnnHoareRuleTac ctxt (i+3),
   50.62                     AnnHoareRuleTac ctxt (i+1)],
   50.63 -             EVERY[rtac (@{thm AnnCond2}) i,
   50.64 +             EVERY[resolve_tac ctxt @{thms AnnCond2} i,
   50.65                     AnnHoareRuleTac ctxt (i+1)],
   50.66 -             EVERY[rtac (@{thm AnnWhile}) i,
   50.67 +             EVERY[resolve_tac ctxt @{thms AnnWhile} i,
   50.68                     AnnHoareRuleTac ctxt (i+2)],
   50.69 -             EVERY[rtac (@{thm AnnAwait}) i,
   50.70 +             EVERY[resolve_tac ctxt @{thms AnnAwait} i,
   50.71                     HoareRuleTac ctxt true (i+1)],
   50.72               K all_tac i]))
   50.73  
   50.74 -and ParallelTac ctxt i = EVERY[rtac (@{thm ParallelRule}) i,
   50.75 +and ParallelTac ctxt i = EVERY[resolve_tac ctxt @{thms ParallelRule} i,
   50.76                            interfree_Tac ctxt (i+1),
   50.77                             MapAnn_Tac ctxt i]
   50.78  
   50.79  and MapAnn_Tac ctxt i st = st |>
   50.80 -    (FIRST[rtac (@{thm MapAnnEmpty}) i,
   50.81 -           EVERY[rtac (@{thm MapAnnList}) i,
   50.82 +    (FIRST[resolve_tac ctxt @{thms MapAnnEmpty} i,
   50.83 +           EVERY[resolve_tac ctxt @{thms MapAnnList} i,
   50.84                   MapAnn_Tac ctxt (i+1),
   50.85                   AnnHoareRuleTac ctxt i],
   50.86 -           EVERY[rtac (@{thm MapAnnMap}) i,
   50.87 -                 rtac (@{thm allI}) i, rtac (@{thm impI}) i,
   50.88 +           EVERY[resolve_tac ctxt @{thms MapAnnMap} i,
   50.89 +                 resolve_tac ctxt @{thms allI} i,
   50.90 +                 resolve_tac ctxt @{thms impI} i,
   50.91                   AnnHoareRuleTac ctxt i]])
   50.92  
   50.93  and interfree_swap_Tac ctxt i st = st |>
   50.94 -    (FIRST[rtac (@{thm interfree_swap_Empty}) i,
   50.95 -           EVERY[rtac (@{thm interfree_swap_List}) i,
   50.96 +    (FIRST[resolve_tac ctxt @{thms interfree_swap_Empty} i,
   50.97 +           EVERY[resolve_tac ctxt @{thms interfree_swap_List} i,
   50.98                   interfree_swap_Tac ctxt (i+2),
   50.99                   interfree_aux_Tac ctxt (i+1),
  50.100                   interfree_aux_Tac ctxt i ],
  50.101 -           EVERY[rtac (@{thm interfree_swap_Map}) i,
  50.102 -                 rtac (@{thm allI}) i,rtac (@{thm impI}) i,
  50.103 -                 conjI_Tac (interfree_aux_Tac ctxt) i]])
  50.104 +           EVERY[resolve_tac ctxt @{thms interfree_swap_Map} i,
  50.105 +                 resolve_tac ctxt @{thms allI} i,
  50.106 +                 resolve_tac ctxt @{thms impI} i,
  50.107 +                 conjI_Tac ctxt (interfree_aux_Tac ctxt) i]])
  50.108  
  50.109  and interfree_Tac ctxt i st = st |>
  50.110 -   (FIRST[rtac (@{thm interfree_Empty}) i,
  50.111 -          EVERY[rtac (@{thm interfree_List}) i,
  50.112 +   (FIRST[resolve_tac ctxt @{thms interfree_Empty} i,
  50.113 +          EVERY[resolve_tac ctxt @{thms interfree_List} i,
  50.114                  interfree_Tac ctxt (i+1),
  50.115                  interfree_swap_Tac ctxt i],
  50.116 -          EVERY[rtac (@{thm interfree_Map}) i,
  50.117 -                rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i,
  50.118 +          EVERY[resolve_tac ctxt @{thms interfree_Map} i,
  50.119 +                resolve_tac ctxt @{thms allI} i,
  50.120 +                resolve_tac ctxt @{thms allI} i,
  50.121 +                resolve_tac ctxt @{thms impI} i,
  50.122                  interfree_aux_Tac ctxt i ]])
  50.123  
  50.124  and interfree_aux_Tac ctxt i = (before_interfree_simp_tac ctxt i ) THEN
  50.125 -        (FIRST[rtac (@{thm interfree_aux_rule1}) i,
  50.126 +        (FIRST[resolve_tac ctxt @{thms interfree_aux_rule1} i,
  50.127                 dest_assertions_Tac ctxt i])
  50.128  
  50.129  and dest_assertions_Tac ctxt i st = st |>
  50.130 -    (FIRST[EVERY[rtac (@{thm AnnBasic_assertions}) i,
  50.131 +    (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_assertions} i,
  50.132                   dest_atomics_Tac ctxt (i+1),
  50.133                   dest_atomics_Tac ctxt i],
  50.134 -           EVERY[rtac (@{thm AnnSeq_assertions}) i,
  50.135 +           EVERY[resolve_tac ctxt @{thms AnnSeq_assertions} i,
  50.136                   dest_assertions_Tac ctxt (i+1),
  50.137                   dest_assertions_Tac ctxt i],
  50.138 -           EVERY[rtac (@{thm AnnCond1_assertions}) i,
  50.139 +           EVERY[resolve_tac ctxt @{thms AnnCond1_assertions} i,
  50.140                   dest_assertions_Tac ctxt (i+2),
  50.141                   dest_assertions_Tac ctxt (i+1),
  50.142                   dest_atomics_Tac ctxt i],
  50.143 -           EVERY[rtac (@{thm AnnCond2_assertions}) i,
  50.144 +           EVERY[resolve_tac ctxt @{thms AnnCond2_assertions} i,
  50.145                   dest_assertions_Tac ctxt (i+1),
  50.146                   dest_atomics_Tac ctxt i],
  50.147 -           EVERY[rtac (@{thm AnnWhile_assertions}) i,
  50.148 +           EVERY[resolve_tac ctxt @{thms AnnWhile_assertions} i,
  50.149                   dest_assertions_Tac ctxt (i+2),
  50.150                   dest_atomics_Tac ctxt (i+1),
  50.151                   dest_atomics_Tac ctxt i],
  50.152 -           EVERY[rtac (@{thm AnnAwait_assertions}) i,
  50.153 +           EVERY[resolve_tac ctxt @{thms AnnAwait_assertions} i,
  50.154                   dest_atomics_Tac ctxt (i+1),
  50.155                   dest_atomics_Tac ctxt i],
  50.156             dest_atomics_Tac ctxt i])
  50.157  
  50.158  and dest_atomics_Tac ctxt i st = st |>
  50.159 -    (FIRST[EVERY[rtac (@{thm AnnBasic_atomics}) i,
  50.160 +    (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_atomics} i,
  50.161                   HoareRuleTac ctxt true i],
  50.162 -           EVERY[rtac (@{thm AnnSeq_atomics}) i,
  50.163 +           EVERY[resolve_tac ctxt @{thms AnnSeq_atomics} i,
  50.164                   dest_atomics_Tac ctxt (i+1),
  50.165                   dest_atomics_Tac ctxt i],
  50.166 -           EVERY[rtac (@{thm AnnCond1_atomics}) i,
  50.167 +           EVERY[resolve_tac ctxt @{thms AnnCond1_atomics} i,
  50.168                   dest_atomics_Tac ctxt (i+1),
  50.169                   dest_atomics_Tac ctxt i],
  50.170 -           EVERY[rtac (@{thm AnnCond2_atomics}) i,
  50.171 +           EVERY[resolve_tac ctxt @{thms AnnCond2_atomics} i,
  50.172                   dest_atomics_Tac ctxt i],
  50.173 -           EVERY[rtac (@{thm AnnWhile_atomics}) i,
  50.174 +           EVERY[resolve_tac ctxt @{thms AnnWhile_atomics} i,
  50.175                   dest_atomics_Tac ctxt i],
  50.176 -           EVERY[rtac (@{thm Annatom_atomics}) i,
  50.177 +           EVERY[resolve_tac ctxt @{thms Annatom_atomics} i,
  50.178                   HoareRuleTac ctxt true i],
  50.179 -           EVERY[rtac (@{thm AnnAwait_atomics}) i,
  50.180 +           EVERY[resolve_tac ctxt @{thms AnnAwait_atomics} i,
  50.181                   HoareRuleTac ctxt true i],
  50.182                   K all_tac i])
  50.183  \<close>
  50.184 @@ -482,18 +486,18 @@
  50.185  text \<open>Tactics useful for dealing with the generated verification conditions:\<close>
  50.186  
  50.187  method_setup conjI_tac = \<open>
  50.188 -  Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac))))\<close>
  50.189 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (conjI_Tac ctxt (K all_tac)))\<close>
  50.190    "verification condition generator for interference freedom tests"
  50.191  
  50.192  ML \<open>
  50.193 -fun disjE_Tac tac i st = st |>
  50.194 -       ( (EVERY [etac disjE i,
  50.195 -          disjE_Tac tac (i+1),
  50.196 +fun disjE_Tac ctxt tac i st = st |>
  50.197 +       ( (EVERY [eresolve_tac ctxt [disjE] i,
  50.198 +          disjE_Tac ctxt tac (i+1),
  50.199            tac i]) ORELSE (tac i) )
  50.200  \<close>
  50.201  
  50.202  method_setup disjE_tac = \<open>
  50.203 -  Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac))))\<close>
  50.204 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (disjE_Tac ctxt (K all_tac)))\<close>
  50.205    "verification condition generator for interference freedom tests"
  50.206  
  50.207  end
    51.1 --- a/src/HOL/IMPP/Com.thy	Sat Jul 18 20:53:05 2015 +0200
    51.2 +++ b/src/HOL/IMPP/Com.thy	Sat Jul 18 20:54:56 2015 +0200
    51.3 @@ -83,7 +83,10 @@
    51.4    "WT_bodies = (!(pn,b):set bodies. WT b)"
    51.5  
    51.6  
    51.7 -ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *}
    51.8 +ML {*
    51.9 +  fun make_imp_tac ctxt =
   51.10 +    EVERY' [resolve_tac ctxt [mp], fn i => assume_tac ctxt (i + 1), eresolve_tac ctxt [thin_rl]]
   51.11 +*}
   51.12  
   51.13  lemma finite_dom_body: "finite (dom body)"
   51.14  apply (unfold body_def)
    52.1 --- a/src/HOL/IMPP/Hoare.thy	Sat Jul 18 20:53:05 2015 +0200
    52.2 +++ b/src/HOL/IMPP/Hoare.thy	Sat Jul 18 20:54:56 2015 +0200
    52.3 @@ -278,7 +278,7 @@
    52.4  
    52.5  lemma hoare_sound: "G||-ts ==> G||=ts"
    52.6  apply (erule hoare_derivs.induct)
    52.7 -apply              (tactic {* TRYALL (eresolve_tac @{context} [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *})
    52.8 +apply              (tactic {* TRYALL (eresolve_tac @{context} [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW assume_tac @{context}) *})
    52.9  apply            (unfold hoare_valids_def)
   52.10  apply            blast
   52.11  apply           blast
   52.12 @@ -351,7 +351,8 @@
   52.13    rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
   52.14    erule_tac [3] conseq12)
   52.15  apply         (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
   52.16 -apply         (tactic {* (rtac @{thm hoare_derivs.If} THEN_ALL_NEW etac @{thm conseq12}) 6 *})
   52.17 +apply         (tactic {* (resolve_tac @{context} @{thms hoare_derivs.If} THEN_ALL_NEW
   52.18 +                eresolve_tac @{context} @{thms conseq12}) 6 *})
   52.19  apply          (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12)
   52.20  apply           auto
   52.21  done
   52.22 @@ -435,7 +436,7 @@
   52.23  apply (frule finite_subset)
   52.24  apply (rule finite_dom_body [THEN finite_imageI])
   52.25  apply (rotate_tac 2)
   52.26 -apply (tactic "make_imp_tac 1")
   52.27 +apply (tactic "make_imp_tac @{context} 1")
   52.28  apply (erule finite_induct)
   52.29  apply  (clarsimp intro!: hoare_derivs.empty)
   52.30  apply (clarsimp intro!: hoare_derivs.insert simp del: range_composition)
    53.1 --- a/src/HOL/IMPP/Natural.thy	Sat Jul 18 20:53:05 2015 +0200
    53.2 +++ b/src/HOL/IMPP/Natural.thy	Sat Jul 18 20:54:56 2015 +0200
    53.3 @@ -111,7 +111,9 @@
    53.4  
    53.5  lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
    53.6  apply (erule evaln.induct)
    53.7 -apply (tactic {* ALLGOALS (resolve_tac @{context} @{thms evalc.intros} THEN_ALL_NEW atac) *})
    53.8 +apply (tactic {*
    53.9 +  ALLGOALS (resolve_tac @{context} @{thms evalc.intros} THEN_ALL_NEW assume_tac @{context})
   53.10 +*})
   53.11  done
   53.12  
   53.13  lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
   53.14 @@ -137,11 +139,12 @@
   53.15  
   53.16  lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
   53.17  apply (erule evalc.induct)
   53.18 -apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
   53.19 -apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac @{context},
   53.20 +apply (tactic {* ALLGOALS (REPEAT o eresolve_tac @{context} [exE]) *})
   53.21 +apply (tactic {* TRYALL (EVERY' [dresolve_tac @{context} @{thms evaln_max2}, assume_tac @{context},
   53.22    REPEAT o eresolve_tac @{context} [exE, conjE]]) *})
   53.23  apply (tactic
   53.24 -  {* ALLGOALS (rtac exI THEN' resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW atac) *})
   53.25 +  {* ALLGOALS (resolve_tac @{context} [exI] THEN'
   53.26 +    resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW assume_tac @{context}) *})
   53.27  done
   53.28  
   53.29  lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
    54.1 --- a/src/HOL/IOA/Solve.thy	Sat Jul 18 20:53:05 2015 +0200
    54.2 +++ b/src/HOL/IOA/Solve.thy	Sat Jul 18 20:54:56 2015 +0200
    54.3 @@ -145,7 +145,7 @@
    54.4    apply force
    54.5    apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
    54.6    apply (tactic {*
    54.7 -    REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE etac conjE 1) THEN
    54.8 +    REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN
    54.9        asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *})
   54.10    done
   54.11  
    55.1 --- a/src/HOL/Import/import_rule.ML	Sat Jul 18 20:53:05 2015 +0200
    55.2 +++ b/src/HOL/Import/import_rule.ML	Sat Jul 18 20:54:56 2015 +0200
    55.3 @@ -220,7 +220,7 @@
    55.4      val tnames = sort_strings (map fst tfrees)
    55.5      val ((_, typedef_info), thy') =
    55.6       Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
    55.7 -       (SOME (Binding.name rep_name, Binding.name abs_name)) (fn _ => rtac th2 1) thy
    55.8 +       (SOME (Binding.name rep_name, Binding.name abs_name)) (fn ctxt => resolve_tac ctxt [th2] 1) thy
    55.9      val aty = #abs_type (#1 typedef_info)
   55.10      val th = freezeT thy' (#type_definition (#2 typedef_info))
   55.11      val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
    56.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Sat Jul 18 20:53:05 2015 +0200
    56.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Sat Jul 18 20:54:56 2015 +0200
    56.3 @@ -54,7 +54,7 @@
    56.4      fun tac [] st = all_tac st
    56.5        | tac (type_enc :: type_encs) st =
    56.6          st (* |> tap (fn _ => tracing (@{make_string} type_enc)) *)
    56.7 -           |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
    56.8 +           |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1)
    56.9                 THEN Metis_Tactic.metis_tac [type_enc]
   56.10                      ATP_Problem_Generate.combsN ctxt ths 1
   56.11                 THEN COND (has_fewer_prems 2) all_tac no_tac
    57.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jul 18 20:53:05 2015 +0200
    57.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jul 18 20:54:56 2015 +0200
    57.3 @@ -178,8 +178,9 @@
    57.4  
    57.5  ML{*
    57.6  fun forward_hyp_tac ctxt =
    57.7 -  ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac ctxt,
    57.8 -    (mp_tac ctxt ORELSE' (dtac spec THEN' mp_tac ctxt)), REPEAT o (etac conjE)]))
    57.9 +  ALLGOALS (TRY o (EVERY' [dresolve_tac ctxt [spec], mp_tac ctxt,
   57.10 +    (mp_tac ctxt ORELSE' (dresolve_tac ctxt [spec] THEN' mp_tac ctxt)),
   57.11 +    REPEAT o (eresolve_tac ctxt [conjE])]))
   57.12  *}
   57.13  
   57.14  
   57.15 @@ -202,7 +203,7 @@
   57.16  apply( tactic "ALLGOALS (REPEAT o resolve_tac @{context} [impI, allI])")
   57.17  apply( tactic {* ALLGOALS (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
   57.18    THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context}))) *})
   57.19 -apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac @{context}])")
   57.20 +apply(tactic "ALLGOALS (EVERY' [REPEAT o (eresolve_tac @{context} [conjE]), REPEAT o hyp_subst_tac @{context}])")
   57.21  
   57.22  -- "Level 7"
   57.23  -- "15 NewC"
   57.24 @@ -241,7 +242,7 @@
   57.25  
   57.26  -- "for FAss"
   57.27  apply( tactic {* EVERY'[eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
   57.28 -       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
   57.29 +       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (eresolve_tac @{context} [conjE]), hyp_subst_tac @{context}] 3*})
   57.30  
   57.31  -- "for if"
   57.32  apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
    58.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 18 20:53:05 2015 +0200
    58.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 18 20:54:56 2015 +0200
    58.3 @@ -127,8 +127,8 @@
    58.4                @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}])
    58.5    fun vector_arith_tac ctxt ths =
    58.6      simp_tac (put_simpset ss1 ctxt)
    58.7 -    THEN' (fn i => rtac @{thm Cartesian_Euclidean_Space.setsum_cong_aux} i
    58.8 -         ORELSE rtac @{thm setsum.neutral} i
    58.9 +    THEN' (fn i => resolve_tac ctxt @{thms Cartesian_Euclidean_Space.setsum_cong_aux} i
   58.10 +         ORELSE resolve_tac ctxt @{thms setsum.neutral} i
   58.11           ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i)
   58.12      (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
   58.13      THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths)
    59.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Sat Jul 18 20:53:05 2015 +0200
    59.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sat Jul 18 20:54:56 2015 +0200
    59.3 @@ -401,6 +401,6 @@
    59.4   fun norm_arith_tac ctxt =
    59.5     clarify_tac (put_claset HOL_cs ctxt) THEN'
    59.6     Object_Logic.full_atomize_tac ctxt THEN'
    59.7 -   CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
    59.8 +   CSUBGOAL ( fn (p,i) => resolve_tac ctxt [norm_arith ctxt (Thm.dest_arg p )] i);
    59.9  
   59.10  end;
    60.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 18 20:53:05 2015 +0200
    60.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 18 20:54:56 2015 +0200
    60.3 @@ -117,10 +117,10 @@
    60.4                val simp1 = @{thm inj_on_def} :: injects;
    60.5                
    60.6                fun proof1 ctxt = EVERY [simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1,
    60.7 -                                          rtac @{thm ballI} 1,
    60.8 -                                          rtac @{thm ballI} 1,
    60.9 -                                          rtac @{thm impI} 1,
   60.10 -                                          atac 1]
   60.11 +                resolve_tac ctxt @{thms ballI} 1,
   60.12 +                resolve_tac ctxt @{thms ballI} 1,
   60.13 +                resolve_tac ctxt @{thms impI} 1,
   60.14 +                assume_tac ctxt 1]
   60.15               
   60.16                val (inj_thm,thy2) = 
   60.17                     add_thms_string [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 (proof1 o #context)), [])] thy1
   60.18 @@ -133,8 +133,8 @@
   60.19                val proof2 = fn {prems, context = ctxt} =>
   60.20                  Induct_Tacs.case_tac ctxt "y" [] NONE 1 THEN
   60.21                  asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
   60.22 -                rtac @{thm exI} 1 THEN
   60.23 -                rtac @{thm refl} 1
   60.24 +                resolve_tac ctxt @{thms exI} 1 THEN
   60.25 +                resolve_tac ctxt @{thms refl} 1
   60.26  
   60.27                (* third statement *)
   60.28                val (inject_thm,thy3) =
   60.29 @@ -149,9 +149,9 @@
   60.30                val simp3 = [@{thm UNIV_def}]
   60.31  
   60.32                fun proof3 ctxt = EVERY [cut_facts_tac inj_thm 1,
   60.33 -                                          dtac @{thm range_inj_infinite} 1,
   60.34 -                                          asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp2) 1,
   60.35 -                                          simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp3) 1]
   60.36 +                dresolve_tac ctxt @{thms range_inj_infinite} 1,
   60.37 +                asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp2) 1,
   60.38 +                simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp3) 1]
   60.39             
   60.40                val (inf_thm,thy4) =  
   60.41                      add_thms_string [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 (proof3 o #context)), [])] thy3
   60.42 @@ -437,7 +437,10 @@
   60.43               fun proof ctxt =
   60.44                simp_tac (put_simpset HOL_basic_ss ctxt
   60.45                    addsimps maps (Global_Theory.get_thms thy') ["cp_def"]) 1
   60.46 -                THEN EVERY [rtac allI 1, rtac allI 1, rtac allI 1, rtac cp1 1];
   60.47 +                THEN EVERY [resolve_tac ctxt [allI] 1,
   60.48 +                  resolve_tac ctxt [allI] 1,
   60.49 +                  resolve_tac ctxt [allI] 1,
   60.50 +                  resolve_tac ctxt [cp1] 1];
   60.51             in
   60.52               yield_singleton add_thms_string ((name,
   60.53                 Goal.prove_global thy' [] [] statement (proof o #context)), []) thy'
   60.54 @@ -504,10 +507,10 @@
   60.55             val at_inst  = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
   60.56  
   60.57             fun proof1 ctxt = EVERY [Class.intro_classes_tac ctxt [],
   60.58 -                                 rtac ((at_inst RS at_pt_inst) RS pt1) 1,
   60.59 -                                 rtac ((at_inst RS at_pt_inst) RS pt2) 1,
   60.60 -                                 rtac ((at_inst RS at_pt_inst) RS pt3) 1,
   60.61 -                                 atac 1];
   60.62 +             resolve_tac ctxt [(at_inst RS at_pt_inst) RS pt1] 1,
   60.63 +             resolve_tac ctxt [(at_inst RS at_pt_inst) RS pt2] 1,
   60.64 +             resolve_tac ctxt [(at_inst RS at_pt_inst) RS pt3] 1,
   60.65 +             assume_tac ctxt 1];
   60.66             fun proof2 ctxt =
   60.67               Class.intro_classes_tac ctxt [] THEN
   60.68               REPEAT (asm_simp_tac
   60.69 @@ -537,7 +540,10 @@
   60.70  
   60.71            fun pt_proof thm ctxt =
   60.72                EVERY [Class.intro_classes_tac ctxt [],
   60.73 -                     rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
   60.74 +                resolve_tac ctxt [thm RS pt1] 1,
   60.75 +                resolve_tac ctxt [thm RS pt2] 1,
   60.76 +                resolve_tac ctxt [thm RS pt3] 1,
   60.77 +                assume_tac ctxt 1];
   60.78  
   60.79            val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
   60.80            val pt_thm_set   = pt_inst RS pt_set_inst;
   60.81 @@ -581,9 +587,10 @@
   60.82             fun proof ctxt =
   60.83                 (if ak_name = ak_name'
   60.84                  then
   60.85 -                  let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst");
   60.86 -                  in  EVERY [Class.intro_classes_tac ctxt [],
   60.87 -                             rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
   60.88 +                  let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst") in
   60.89 +                    EVERY [Class.intro_classes_tac ctxt [],
   60.90 +                      resolve_tac ctxt [(at_thm RS fs_at_inst) RS fs1] 1]
   60.91 +                  end
   60.92                  else
   60.93                    let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
   60.94                        val simp_s =
   60.95 @@ -605,7 +612,8 @@
   60.96          let
   60.97            val cls_name = Sign.full_bname thy ("fs_"^ak_name);
   60.98            val fs_inst  = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst");
   60.99 -          fun fs_proof thm ctxt = EVERY [Class.intro_classes_tac ctxt [], rtac (thm RS fs1) 1];
  60.100 +          fun fs_proof thm ctxt =
  60.101 +            EVERY [Class.intro_classes_tac ctxt [], resolve_tac ctxt [thm RS fs1] 1];
  60.102  
  60.103            val fs_thm_unit  = fs_unit_inst;
  60.104            val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
  60.105 @@ -652,7 +660,7 @@
  60.106                      val at_inst  = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst");
  60.107                    in
  60.108                     EVERY [Class.intro_classes_tac ctxt [],
  60.109 -                          rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
  60.110 +                     resolve_tac ctxt [at_inst RS (pt_inst RS pt_perm_compose)] 1]
  60.111                    end)
  60.112                  else
  60.113                    (let
  60.114 @@ -686,7 +694,8 @@
  60.115              val pt_inst  = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst");
  60.116              val at_inst  = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst");
  60.117  
  60.118 -            fun cp_proof thm ctxt = EVERY [Class.intro_classes_tac ctxt [], rtac (thm RS cp1) 1];
  60.119 +            fun cp_proof thm ctxt =
  60.120 +              EVERY [Class.intro_classes_tac ctxt [], resolve_tac ctxt [thm RS cp1] 1];
  60.121            
  60.122              val cp_thm_unit = cp_unit_inst;
  60.123              val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
    61.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jul 18 20:53:05 2015 +0200
    61.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jul 18 20:54:56 2015 +0200
    61.3 @@ -586,7 +586,9 @@
    61.4              (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
    61.5              (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    61.6                 Const (cname, U --> HOLogic.boolT)) NONE
    61.7 -            (fn ctxt => rtac exI 1 THEN rtac CollectI 1 THEN
    61.8 +            (fn ctxt =>
    61.9 +              resolve_tac ctxt [exI] 1 THEN
   61.10 +              resolve_tac ctxt [CollectI] 1 THEN
   61.11                QUIET_BREADTH_FIRST (has_fewer_prems 1)
   61.12                (resolve_tac ctxt rep_intrs 1)) thy |> (fn ((_, r), thy) =>
   61.13          let
   61.14 @@ -663,8 +665,8 @@
   61.15                   (if atom1 = atom2 then []
   61.16                    else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
   61.17                cong_tac ctxt 1,
   61.18 -              rtac refl 1,
   61.19 -              rtac cp1' 1]) thy)
   61.20 +              resolve_tac ctxt [refl] 1,
   61.21 +              resolve_tac ctxt [cp1'] 1]) thy)
   61.22          (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
   61.23             tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy
   61.24        end;
   61.25 @@ -812,7 +814,7 @@
   61.26        in Goal.prove_global_future thy8 [] [] eqn (fn {context = ctxt, ...} => EVERY
   61.27          [resolve_tac ctxt inj_thms 1,
   61.28           rewrite_goals_tac ctxt rewrites,
   61.29 -         rtac refl 3,
   61.30 +         resolve_tac ctxt [refl] 3,
   61.31           resolve_tac ctxt rep_intrs 2,
   61.32           REPEAT (resolve_tac ctxt Rep_thms 1)])
   61.33        end;
   61.34 @@ -1046,11 +1048,12 @@
   61.35          (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_prems),
   61.36           HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_concls)))
   61.37           (fn {context = ctxt, ...} => EVERY
   61.38 -           [REPEAT (etac conjE 1),
   61.39 +           [REPEAT (eresolve_tac ctxt [conjE] 1),
   61.40              REPEAT (EVERY
   61.41 -              [TRY (rtac conjI 1),
   61.42 +              [TRY (resolve_tac ctxt [conjI] 1),
   61.43                 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps Rep_inverse_thms) 1,
   61.44 -               etac mp 1, resolve_tac ctxt Rep_thms 1])]);
   61.45 +               eresolve_tac ctxt [mp] 1,
   61.46 +               resolve_tac ctxt Rep_thms 1])]);
   61.47  
   61.48      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma)));
   61.49      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   61.50 @@ -1064,7 +1067,7 @@
   61.51      val dt_induct = Goal.prove_global_future thy8 []
   61.52        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   61.53        (fn {prems, context = ctxt} => EVERY
   61.54 -        [rtac indrule_lemma' 1,
   61.55 +        [resolve_tac ctxt [indrule_lemma'] 1,
   61.56           (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
   61.57             Object_Logic.atomize_prems_tac ctxt) 1,
   61.58           EVERY (map (fn (prem, r) => (EVERY
   61.59 @@ -1262,9 +1265,9 @@
   61.60                 fin_set_supp @ ths)) 1]);
   61.61          val (([(_, cx)], ths), ctxt') = Obtain.result
   61.62            (fn ctxt' => EVERY
   61.63 -            [etac exE 1,
   61.64 +            [eresolve_tac ctxt' [exE] 1,
   61.65               full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1,
   61.66 -             REPEAT (etac conjE 1)])
   61.67 +             REPEAT (eresolve_tac ctxt' [conjE] 1)])
   61.68            [ex] ctxt
   61.69        in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end;
   61.70  
   61.71 @@ -1320,7 +1323,7 @@
   61.72               EVERY (Old_Datatype_Aux.ind_tac context1 dt_induct tnames 1 ::
   61.73                 maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
   61.74                   map (fn ((cname, cargs), is) =>
   61.75 -                   REPEAT (rtac allI 1) THEN
   61.76 +                   REPEAT (resolve_tac context1 [allI] 1) THEN
   61.77                     SUBPROOF (fn {prems = iprems, params, concl,
   61.78                         context = context2, ...} =>
   61.79                       let
   61.80 @@ -1354,14 +1357,15 @@
   61.81                                list_comb (cnstr, maps (fn ((bs, t), cs) =>
   61.82                                  cs @ [fold_rev (mk_perm []) (map perm_of_pair
   61.83                                    (bs ~~ cs)) t]) (xs'' ~~ freshs1')))))
   61.84 -                           (fn _ => EVERY
   61.85 +                           (fn {context = ctxt, ...} => EVERY
   61.86                                (simp_tac (put_simpset HOL_ss context3 addsimps flat inject_thms) 1 ::
   61.87 -                               REPEAT (FIRSTGOAL (rtac conjI)) ::
   61.88 +                               REPEAT (FIRSTGOAL (resolve_tac ctxt [conjI])) ::
   61.89                                 maps (fn ((bs, t), cs) =>
   61.90                                   if null bs then []
   61.91 -                                 else rtac sym 1 :: maps (fn (b, c) =>
   61.92 -                                   [rtac trans 1, rtac sym 1,
   61.93 -                                    rtac (fresh_fresh_inst thy9 b c) 1,
   61.94 +                                 else resolve_tac ctxt [sym] 1 :: maps (fn (b, c) =>
   61.95 +                                   [resolve_tac ctxt [trans] 1,
   61.96 +                                    resolve_tac ctxt [sym] 1,
   61.97 +                                    resolve_tac ctxt [fresh_fresh_inst thy9 b c] 1,
   61.98                                      simp_tac ind_ss1' 1,
   61.99                                      simp_tac ind_ss2 1,
  61.100                                      simp_tac ind_ss3' 1]) (bs ~~ cs))
  61.101 @@ -1385,8 +1389,8 @@
  61.102          EVERY
  61.103            [cut_facts_tac [th] 1,
  61.104             REPEAT (eresolve_tac context [conjE, @{thm allE_Nil}] 1),
  61.105 -           REPEAT (etac allE 1),
  61.106 -           REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)]
  61.107 +           REPEAT (eresolve_tac context [allE] 1),
  61.108 +           REPEAT (TRY (resolve_tac context [conjI] 1) THEN asm_full_simp_tac ind_ss5 1)]
  61.109        end);
  61.110  
  61.111      val induct_aux' = Thm.instantiate ([],
  61.112 @@ -1404,10 +1408,10 @@
  61.113        (map (augment_sort thy9 fs_cp_sort) ind_prems)
  61.114        (augment_sort thy9 fs_cp_sort ind_concl)
  61.115        (fn {prems, context = ctxt} => EVERY
  61.116 -         [rtac induct_aux' 1,
  61.117 +         [resolve_tac ctxt [induct_aux'] 1,
  61.118            REPEAT (resolve_tac ctxt fs_atoms 1),
  61.119            REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW
  61.120 -            (etac @{thm meta_spec} ORELSE'
  61.121 +            (eresolve_tac ctxt @{thms meta_spec} ORELSE'
  61.122                full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [fresh_def]))) 1)])
  61.123  
  61.124      val (_, thy10) = thy9 |>
  61.125 @@ -1551,7 +1555,8 @@
  61.126              (Goal.prove_global_future thy11 [] []
  61.127                (augment_sort thy1 pt_cp_sort
  61.128                  (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
  61.129 -              (fn {context = ctxt, ...} => rtac rec_induct 1 THEN REPEAT
  61.130 +              (fn {context = ctxt, ...} =>
  61.131 +                 resolve_tac ctxt [rec_induct] 1 THEN REPEAT
  61.132                   (simp_tac (put_simpset HOL_basic_ss ctxt
  61.133                      addsimps flat perm_simps'
  61.134                      addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
  61.135 @@ -1561,9 +1566,10 @@
  61.136            Goal.prove_global_future thy11 [] []
  61.137              (augment_sort thy1 pt_cp_sort
  61.138                (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
  61.139 -            (fn {context = ctxt, ...} => dtac (Thm.instantiate ([],
  61.140 +            (fn {context = ctxt, ...} =>
  61.141 +              dresolve_tac ctxt [Thm.instantiate ([],
  61.142                   [((("pi", 0), permT),
  61.143 -                   Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN
  61.144 +                   Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th] 1 THEN
  61.145                 NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
  61.146        in (ths, ths') end) dt_atomTs);
  61.147  
  61.148 @@ -1594,7 +1600,7 @@
  61.149                     end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
  61.150                       (1 upto length recTs))))))
  61.151              (fn {prems = fins, context = ctxt} =>
  61.152 -              (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
  61.153 +              (resolve_tac ctxt [rec_induct] THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
  61.154                 (NominalPermeq.finite_guess_tac (put_simpset HOL_ss ctxt addsimps [fs_name]) 1))))
  61.155        end) dt_atomTs;
  61.156  
  61.157 @@ -1640,25 +1646,25 @@
  61.158                     val _ $ (_ $ (_ $ S $ _)) $ _ = Thm.prop_of supports_fresh;
  61.159                     val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns')
  61.160                   in EVERY
  61.161 -                   [rtac (Drule.cterm_instantiate
  61.162 +                   [resolve_tac context [Drule.cterm_instantiate
  61.163                        [(Thm.global_cterm_of thy11 S,
  61.164                          Thm.global_cterm_of thy11 (Const (@{const_name Nominal.supp},
  61.165                            fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
  61.166 -                      supports_fresh) 1,
  61.167 +                      supports_fresh] 1,
  61.168                      simp_tac (put_simpset HOL_basic_ss context addsimps
  61.169                        [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1,
  61.170                      REPEAT_DETERM (resolve_tac context [allI, impI] 1),
  61.171 -                    REPEAT_DETERM (etac conjE 1),
  61.172 -                    rtac unique 1,
  61.173 -                    SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
  61.174 -                      [cut_facts_tac [rec_prem] 1,
  61.175 -                       rtac (Thm.instantiate ([],
  61.176 +                    REPEAT_DETERM (eresolve_tac context [conjE] 1),
  61.177 +                    resolve_tac context [unique] 1,
  61.178 +                    SUBPROOF (fn {context = ctxt, prems = prems', params = [(_, a), (_, b)], ...} =>
  61.179 +                      EVERY [cut_facts_tac [rec_prem] 1,
  61.180 +                       resolve_tac ctxt [Thm.instantiate ([],
  61.181                           [((("pi", 0), mk_permT aT),
  61.182                             Thm.global_cterm_of thy11
  61.183 -                            (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1,
  61.184 +                            (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th] 1,
  61.185                         asm_simp_tac (put_simpset HOL_ss context addsimps
  61.186                           (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1,
  61.187 -                    rtac rec_prem 1,
  61.188 +                    resolve_tac context [rec_prem] 1,
  61.189                      simp_tac (put_simpset HOL_ss context addsimps (fs_name ::
  61.190                        supp_prod :: finite_Un :: finite_prems)) 1,
  61.191                      simp_tac (put_simpset HOL_ss context addsimps (Thm.symmetric fresh_def ::
  61.192 @@ -1705,10 +1711,10 @@
  61.193               resolve_tac ctxt exists_fresh' 1,
  61.194               asm_simp_tac (put_simpset HOL_ss ctxt addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
  61.195          val (([(_, cx)], ths), ctxt') = Obtain.result
  61.196 -          (fn _ => EVERY
  61.197 -            [etac exE 1,
  61.198 -             full_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_prod :: fresh_atm)) 1,
  61.199 -             REPEAT (etac conjE 1)])
  61.200 +          (fn ctxt' => EVERY
  61.201 +            [eresolve_tac ctxt' [exE] 1,
  61.202 +             full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1,
  61.203 +             REPEAT (eresolve_tac ctxt [conjE] 1)])
  61.204            [ex] ctxt
  61.205        in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end;
  61.206  
  61.207 @@ -1740,13 +1746,13 @@
  61.208                          (rec_unique_frees'' ~~ rec_unique_frees' ~~
  61.209                             rec_sets ~~ rec_preds)))))
  61.210                 (fn {context = ctxt, ...} =>
  61.211 -                  rtac rec_induct 1 THEN
  61.212 +                  resolve_tac ctxt [rec_induct] 1 THEN
  61.213                    REPEAT ((resolve_tac ctxt P_ind_ths THEN_ALL_NEW assume_tac ctxt) 1))));
  61.214             val rec_fin_supp_thms' = map
  61.215               (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
  61.216               (rec_fin_supp_thms ~~ finite_thss);
  61.217           in EVERY
  61.218 -           ([rtac induct_aux_rec 1] @
  61.219 +           ([resolve_tac context [induct_aux_rec] 1] @
  61.220              maps (fn ((_, finite_ths), finite_th) =>
  61.221                [cut_facts_tac (finite_th :: finite_ths) 1,
  61.222                 asm_simp_tac (put_simpset HOL_ss context addsimps [supp_prod, finite_Un]) 1])
  61.223 @@ -1754,10 +1760,10 @@
  61.224              maps (fn ((_, idxss), elim) => maps (fn idxs =>
  61.225                [full_simp_tac (put_simpset HOL_ss context addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
  61.226                 REPEAT_DETERM (eresolve_tac context @{thms conjE ex1E} 1),
  61.227 -               rtac @{thm ex1I} 1,
  61.228 -               (resolve_tac context rec_intrs THEN_ALL_NEW atac) 1,
  61.229 +               resolve_tac context @{thms ex1I} 1,
  61.230 +               (resolve_tac context rec_intrs THEN_ALL_NEW assume_tac context) 1,
  61.231                 rotate_tac ~1 1,
  61.232 -               ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
  61.233 +               ((DETERM o eresolve_tac context [elim]) THEN_ALL_NEW full_simp_tac
  61.234                    (put_simpset HOL_ss context addsimps flat distinct_thms)) 1] @
  61.235                 (if null idxs then [] else [hyp_subst_tac context 1,
  61.236                  SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
  61.237 @@ -1825,10 +1831,10 @@
  61.238                      val pi1_pi2_eq = Goal.prove context'' [] []
  61.239                        (HOLogic.mk_Trueprop (HOLogic.mk_eq
  61.240                          (fold_rev (mk_perm []) pi1 lhs, fold_rev (mk_perm []) pi2 rhs)))
  61.241 -                      (fn _ => EVERY
  61.242 +                      (fn {context = ctxt, ...} => EVERY
  61.243                           [cut_facts_tac constr_fresh_thms 1,
  61.244                            asm_simp_tac (put_simpset HOL_basic_ss context'' addsimps perm_fresh_fresh) 1,
  61.245 -                          rtac prem 1]);
  61.246 +                          resolve_tac ctxt [prem] 1]);
  61.247  
  61.248                      (** pi1 o ts = pi2 o us **)
  61.249                      val _ = warning "step 4: pi1 o ts = pi2 o us";
  61.250 @@ -1866,21 +1872,21 @@
  61.251                          val k = find_index (equal s) rec_set_names;
  61.252                          val pi = rpi1 @ pi2;
  61.253                          fun mk_pi z = fold_rev (mk_perm []) pi z;
  61.254 -                        fun eqvt_tac p =
  61.255 +                        fun eqvt_tac ctxt p =
  61.256                            let
  61.257                              val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
  61.258                              val l = find_index (equal T) dt_atomTs;
  61.259                              val th = nth (nth rec_equiv_thms' l) k;
  61.260                              val th' = Thm.instantiate ([],
  61.261                                [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th;
  61.262 -                          in rtac th' 1 end;
  61.263 +                          in resolve_tac ctxt [th'] 1 end;
  61.264                          val th' = Goal.prove context'' [] []
  61.265                            (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
  61.266 -                          (fn _ => EVERY
  61.267 -                             (map eqvt_tac pi @
  61.268 +                          (fn {context = ctxt, ...} => EVERY
  61.269 +                             (map (eqvt_tac ctxt) pi @
  61.270                                [simp_tac (put_simpset HOL_ss context'' addsimps (fresh_prems' @ freshs2' @
  61.271                                   perm_swap @ perm_fresh_fresh)) 1,
  61.272 -                               rtac th 1]))
  61.273 +                               resolve_tac ctxt [th] 1]))
  61.274                        in
  61.275                          Simplifier.simplify
  61.276                            (put_simpset HOL_basic_ss context'' addsimps rpi1_pi2_eqs) th'
  61.277 @@ -1924,12 +1930,13 @@
  61.278                              in
  61.279                                Goal.prove context'' [] []
  61.280                                  (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y))
  61.281 -                                (fn _ => EVERY
  61.282 -                                   (rtac (nth (nth rec_fresh_thms l) k) 1 ::
  61.283 -                                    map (fn th => rtac th 1)
  61.284 +                                (fn {context = ctxt, ...} => EVERY
  61.285 +                                   (resolve_tac ctxt [nth (nth rec_fresh_thms l) k] 1 ::
  61.286 +                                    map (fn th => resolve_tac ctxt [th] 1)
  61.287                                        (snd (nth finite_thss l)) @
  61.288 -                                    [rtac rec_prem 1, rtac ih 1,
  61.289 -                                     REPEAT_DETERM (resolve_tac context fresh_prems 1)]))
  61.290 +                                    [resolve_tac ctxt [rec_prem] 1,
  61.291 +                                     resolve_tac ctxt [ih] 1,
  61.292 +                                     REPEAT_DETERM (resolve_tac ctxt fresh_prems 1)]))
  61.293                              end) atoms
  61.294                          end) (rec_prems1 ~~ ihs);
  61.295  
  61.296 @@ -1954,8 +1961,9 @@
  61.297                          (HOLogic.mk_Trueprop (fresh_const aT rT $
  61.298                              fold_rev (mk_perm []) (rpi2 @ pi1) a $
  61.299                              fold_rev (mk_perm []) (rpi2 @ pi1) rhs'))
  61.300 -                        (fn _ => simp_tac (put_simpset HOL_ss context'' addsimps fresh_bij) 1 THEN
  61.301 -                           rtac th 1)
  61.302 +                        (fn {context = ctxt, ...} =>
  61.303 +                          simp_tac (put_simpset HOL_ss context'' addsimps fresh_bij) 1 THEN
  61.304 +                          resolve_tac ctxt [th] 1)
  61.305                        in
  61.306                          Goal.prove context'' [] []
  61.307                            (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
  61.308 @@ -2048,14 +2056,14 @@
  61.309          val prems' = flat finite_premss @ finite_ctxt_prems @
  61.310            rec_prems @ rec_prems' @ map (subst_atomic ps) prems;
  61.311          fun solve ctxt rules prems = resolve_tac ctxt rules THEN_ALL_NEW
  61.312 -          (resolve_tac ctxt prems THEN_ALL_NEW atac)
  61.313 +          (resolve_tac ctxt prems THEN_ALL_NEW assume_tac ctxt)
  61.314        in
  61.315          Goal.prove_global_future thy12 []
  61.316            (map (augment_sort thy12 fs_cp_sort) prems')
  61.317            (augment_sort thy12 fs_cp_sort concl')
  61.318            (fn {context = ctxt, prems} => EVERY
  61.319              [rewrite_goals_tac ctxt reccomb_defs,
  61.320 -             rtac @{thm the1_equality} 1,
  61.321 +             resolve_tac ctxt @{thms the1_equality} 1,
  61.322               solve ctxt rec_unique_thms prems 1,
  61.323               resolve_tac ctxt rec_intrs 1,
  61.324               REPEAT (solve ctxt (prems @ rec_total_thms) prems 1)])
    62.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jul 18 20:53:05 2015 +0200
    62.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jul 18 20:54:56 2015 +0200
    62.3 @@ -79,8 +79,8 @@
    62.4   in
    62.5     fn st =>
    62.6     (cut_inst_tac_term' ctxt [(x,s)] exists_fresh' 1 THEN
    62.7 -   rtac fs_name_thm 1 THEN
    62.8 -   etac exE 1) st
    62.9 +   resolve_tac ctxt [fs_name_thm] 1 THEN
   62.10 +   eresolve_tac ctxt [exE] 1) st
   62.11    handle List.Empty  => all_tac st (* if we collected no variables then we do nothing *)
   62.12   end) 1;
   62.13  
   62.14 @@ -163,8 +163,8 @@
   62.15      (* The tactics which solve the subgoals generated
   62.16         by the conditionnal rewrite rule. *)
   62.17      val post_rewrite_tacs =
   62.18 -          [rtac pt_name_inst,
   62.19 -           rtac at_name_inst,
   62.20 +          [resolve_tac ctxt [pt_name_inst],
   62.21 +           resolve_tac ctxt [at_name_inst],
   62.22             TRY o SOLVED' (NominalPermeq.finite_guess_tac simp_ctxt),
   62.23             inst_fresh vars params THEN'
   62.24             (TRY o SOLVED' (NominalPermeq.fresh_guess_tac simp_ctxt)) THEN'
    63.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Jul 18 20:53:05 2015 +0200
    63.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jul 18 20:54:56 2015 +0200
    63.3 @@ -121,7 +121,7 @@
    63.4                (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
    63.5              |> Seq.maps (fn rule' =>
    63.6                CASES (rule_cases ctxt rule' cases)
    63.7 -                (rtac (rename_params_rule false [] rule') i THEN
    63.8 +                (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN
    63.9                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
   63.10      THEN_ALL_NEW_CASES
   63.11        ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
    64.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Jul 18 20:53:05 2015 +0200
    64.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Jul 18 20:54:56 2015 +0200
    64.3 @@ -104,8 +104,8 @@
    64.4    | inst_conj_all _ _ _ _ _ = NONE;
    64.5  
    64.6  fun inst_conj_all_tac ctxt k = EVERY
    64.7 -  [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
    64.8 -   REPEAT_DETERM_N k (etac allE 1),
    64.9 +  [TRY (EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [conjI] 1, assume_tac ctxt 1]),
   64.10 +   REPEAT_DETERM_N k (eresolve_tac ctxt [allE] 1),
   64.11     simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]) 1];
   64.12  
   64.13  fun map_term f t u = (case f t u of
   64.14 @@ -129,9 +129,9 @@
   64.15      val prop = Thm.prop_of th;
   64.16      fun prove t =
   64.17        Goal.prove ctxt [] [] t (fn _ =>
   64.18 -        EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
   64.19 +        EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1,
   64.20            REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
   64.21 -          REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
   64.22 +          REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))])
   64.23    in Option.map prove (map_term f prop (the_default prop opt)) end;
   64.24  
   64.25  val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion;
   64.26 @@ -300,19 +300,20 @@
   64.27               resolve_tac ctxt fs_atoms 1]);
   64.28          val (([(_, cx)], ths), ctxt') = Obtain.result
   64.29            (fn ctxt' => EVERY
   64.30 -            [etac exE 1,
   64.31 +            [eresolve_tac ctxt' [exE] 1,
   64.32               full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1,
   64.33               full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1,
   64.34 -             REPEAT (etac conjE 1)])
   64.35 +             REPEAT (eresolve_tac ctxt [conjE] 1)])
   64.36            [ex] ctxt
   64.37        in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end;
   64.38  
   64.39      fun mk_ind_proof ctxt' thss =
   64.40        Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
   64.41          let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
   64.42 -          rtac raw_induct 1 THEN
   64.43 +          resolve_tac context [raw_induct] 1 THEN
   64.44            EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
   64.45 -            [REPEAT (rtac allI 1), simp_tac (put_simpset eqvt_ss context) 1,
   64.46 +            [REPEAT (resolve_tac context [allI] 1),
   64.47 +             simp_tac (put_simpset eqvt_ss context) 1,
   64.48               SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
   64.49                 let
   64.50                   val (params', (pis, z)) =
   64.51 @@ -354,7 +355,7 @@
   64.52                        if null (preds_of ps t) then (SOME th, mk_pi th)
   64.53                        else
   64.54                          (map_thm ctxt' (split_conj (K o I) names)
   64.55 -                           (etac conjunct1 1) monos NONE th,
   64.56 +                           (eresolve_tac ctxt' [conjunct1] 1) monos NONE th,
   64.57                           mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
   64.58                             (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th))))
   64.59                        (gprems ~~ oprems)) |>> map_filter I;
   64.60 @@ -370,7 +371,7 @@
   64.61                           (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs)
   64.62                              (fold_rev (NominalDatatype.mk_perm []) pis rhs)))
   64.63                         (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps
   64.64 -                          (fresh_bij @ perm_bij)) 1 THEN rtac th' 1)
   64.65 +                          (fresh_bij @ perm_bij)) 1 THEN resolve_tac ctxt' [th'] 1)
   64.66                     in Simplifier.simplify (put_simpset eqvt_ss ctxt'' addsimps fresh_atm) th'' end)
   64.67                       vc_compat_ths;
   64.68                   val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths';
   64.69 @@ -382,7 +383,8 @@
   64.70                   val th = Goal.prove ctxt'' [] []
   64.71                     (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
   64.72                       map (fold (NominalDatatype.mk_perm []) pis') (tl ts))))
   64.73 -                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, rtac ihyp' 1,
   64.74 +                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1,
   64.75 +                     resolve_tac ctxt'' [ihyp'] 1,
   64.76                       REPEAT_DETERM_N (Thm.nprems_of ihyp - length gprems)
   64.77                         (simp_tac swap_simps_simpset 1),
   64.78                       REPEAT_DETERM_N (length gprems)
   64.79 @@ -398,9 +400,10 @@
   64.80                 in resolve_tac ctxt' final' 1 end) context 1])
   64.81                   (prems ~~ thss ~~ ihyps ~~ prems'')))
   64.82          in
   64.83 -          cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
   64.84 +          cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt [conjE] 1) THEN
   64.85            REPEAT (REPEAT (resolve_tac ctxt [conjI, impI] 1) THEN
   64.86 -            etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
   64.87 +            eresolve_tac ctxt [impE] 1 THEN assume_tac ctxt 1 THEN
   64.88 +            REPEAT (eresolve_tac ctxt @{thms allE_Nil} 1) THEN
   64.89              asm_full_simp_tac ctxt 1)
   64.90          end) |> singleton (Proof_Context.export ctxt' ctxt);
   64.91  
   64.92 @@ -466,11 +469,11 @@
   64.93          prems') =
   64.94        (name, Goal.prove ctxt' [] (prem :: prems') concl
   64.95          (fn {prems = hyp :: hyps, context = ctxt1} =>
   64.96 -        EVERY (rtac (hyp RS elim) 1 ::
   64.97 +        EVERY (resolve_tac ctxt1 [hyp RS elim] 1 ::
   64.98            map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
   64.99              SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} =>
  64.100                if null qs then
  64.101 -                rtac (first_order_mrs case_hyps case_hyp) 1
  64.102 +                resolve_tac ctxt2 [first_order_mrs case_hyps case_hyp] 1
  64.103                else
  64.104                  let
  64.105                    val params' = map (Thm.term_of o #2 o nth (rev params)) is;
  64.106 @@ -518,8 +521,8 @@
  64.107                      (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj);
  64.108                    val th = Goal.prove ctxt3 [] [] (Thm.term_of concl)
  64.109                      (fn {context = ctxt4, ...} =>
  64.110 -                       rtac (Thm.instantiate inst case_hyp) 1 THEN
  64.111 -                       SUBPROOF (fn {prems = fresh_hyps, ...} =>
  64.112 +                       resolve_tac ctxt4 [Thm.instantiate inst case_hyp] 1 THEN
  64.113 +                       SUBPROOF (fn {context = ctxt5, prems = fresh_hyps, ...} =>
  64.114                           let
  64.115                             val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps;
  64.116                             val case_simpset = cases_eqvt_simpset addsimps freshs2' @
  64.117 @@ -532,8 +535,8 @@
  64.118                             val case_hyps' = hyps1' @ hyps2'
  64.119                           in
  64.120                             simp_tac case_simpset 1 THEN
  64.121 -                           REPEAT_DETERM (TRY (rtac conjI 1) THEN
  64.122 -                             resolve_tac ctxt4 case_hyps' 1)
  64.123 +                           REPEAT_DETERM (TRY (resolve_tac ctxt5 [conjI] 1) THEN
  64.124 +                             resolve_tac ctxt5 case_hyps' 1)
  64.125                           end) ctxt4 1)
  64.126                    val final = Proof_Context.export ctxt3 ctxt2 [th]
  64.127                  in resolve_tac ctxt2 final 1 end) ctxt1 1)
  64.128 @@ -629,13 +632,13 @@
  64.129          val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
  64.130            let
  64.131              val prems' = map (fn th => the_default th (map_thm ctxt''
  64.132 -              (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
  64.133 +              (split_conj (K I) names) (eresolve_tac ctxt'' [conjunct2] 1) monos NONE th)) prems;
  64.134              val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
  64.135                (mk_perm_bool (Thm.global_cterm_of thy pi) th)) prems';
  64.136              val intr' = Drule.cterm_instantiate (map (Thm.global_cterm_of thy) vs ~~
  64.137                 map (Thm.global_cterm_of thy o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
  64.138                 intr
  64.139 -          in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
  64.140 +          in (resolve_tac ctxt'' [intr'] THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
  64.141            end) ctxt' 1 st
  64.142        in
  64.143          case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
  64.144 @@ -655,7 +658,7 @@
  64.145                HOLogic.mk_imp (p, list_comb (h, ts1 @
  64.146                  map (NominalDatatype.mk_perm [] pi') ts2))
  64.147              end) ps)))
  64.148 -          (fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
  64.149 +          (fn _ => EVERY (resolve_tac ctxt' [raw_induct] 1 :: map (fn intr_vs =>
  64.150                full_simp_tac eqvt_simpset 1 THEN
  64.151                eqvt_tac pi' intr_vs) intrs')) |>
  64.152            singleton (Proof_Context.export ctxt' ctxt)))
    65.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Jul 18 20:53:05 2015 +0200
    65.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Jul 18 20:54:56 2015 +0200
    65.3 @@ -109,8 +109,8 @@
    65.4    | inst_conj_all _ _ _ _ _ = NONE;
    65.5  
    65.6  fun inst_conj_all_tac ctxt k = EVERY
    65.7 -  [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
    65.8 -   REPEAT_DETERM_N k (etac allE 1),
    65.9 +  [TRY (EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [conjI] 1, assume_tac ctxt 1]),
   65.10 +   REPEAT_DETERM_N k (eresolve_tac ctxt [allE] 1),
   65.11     simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]) 1];
   65.12  
   65.13  fun map_term f t u = (case f t u of
   65.14 @@ -134,9 +134,9 @@
   65.15      val prop = Thm.prop_of th;
   65.16      fun prove t =
   65.17        Goal.prove ctxt [] [] t (fn _ =>
   65.18 -        EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
   65.19 +        EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1,
   65.20            REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
   65.21 -          REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
   65.22 +          REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))])
   65.23    in Option.map prove (map_term f prop (the_default prop opt)) end;
   65.24  
   65.25  fun abs_params params t =
   65.26 @@ -321,11 +321,11 @@
   65.27            ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
   65.28          val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
   65.29            (fn ctxt' => EVERY
   65.30 -            [rtac avoid_th 1,
   65.31 +            [resolve_tac ctxt' [avoid_th] 1,
   65.32               full_simp_tac (put_simpset HOL_ss ctxt' addsimps [@{thm fresh_star_prod_set}]) 1,
   65.33               full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1,
   65.34               rotate_tac 1 1,
   65.35 -             REPEAT (etac conjE 1)])
   65.36 +             REPEAT (eresolve_tac ctxt' [conjE] 1)])
   65.37            [] ctxt;
   65.38          val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets);
   65.39          val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2);
   65.40 @@ -348,10 +348,10 @@
   65.41      fun mk_ind_proof ctxt' thss =
   65.42        Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
   65.43          let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
   65.44 -          rtac raw_induct 1 THEN
   65.45 +          resolve_tac ctxt [raw_induct] 1 THEN
   65.46            EVERY (maps (fn (((((_, sets, oprems, _),
   65.47                vc_compat_ths), vc_compat_vs), ihyp), vs_ihypt) =>
   65.48 -            [REPEAT (rtac allI 1), simp_tac (put_simpset eqvt_ss context) 1,
   65.49 +            [REPEAT (resolve_tac ctxt [allI] 1), simp_tac (put_simpset eqvt_ss context) 1,
   65.50               SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
   65.51                 let
   65.52                   val (cparams', (pis, z)) =
   65.53 @@ -366,7 +366,7 @@
   65.54                     if null (preds_of ps t) then SOME th
   65.55                     else
   65.56                       map_thm ctxt' (split_conj (K o I) names)
   65.57 -                       (etac conjunct1 1) monos NONE th)
   65.58 +                       (eresolve_tac ctxt' [conjunct1] 1) monos NONE th)
   65.59                     (gprems ~~ oprems);
   65.60                   val vc_compat_ths' = map2 (fn th => fn p =>
   65.61                     let
   65.62 @@ -378,7 +378,7 @@
   65.63                         (HOLogic.mk_Trueprop (list_comb (h,
   65.64                            map (fold_rev (NominalDatatype.mk_perm []) pis) ts)))
   65.65                         (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt' addsimps
   65.66 -                          (fresh_star_bij @ finite_ineq)) 1 THEN rtac th' 1)
   65.67 +                          (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac ctxt' [th'] 1)
   65.68                     end) vc_compat_ths vc_compat_vs;
   65.69                   val (vc_compat_ths1, vc_compat_ths2) =
   65.70                     chop (length vc_compat_ths - length sets) vc_compat_ths';
   65.71 @@ -416,8 +416,9 @@
   65.72                   val th = Goal.prove ctxt'' [] []
   65.73                     (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
   65.74                       map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts))))
   65.75 -                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, rtac ihyp' 1] @
   65.76 -                     map (fn th => rtac th 1) fresh_ths3 @
   65.77 +                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1,
   65.78 +                     resolve_tac ctxt'' [ihyp'] 1] @
   65.79 +                     map (fn th => resolve_tac ctxt'' [th] 1) fresh_ths3 @
   65.80                       [REPEAT_DETERM_N (length gprems)
   65.81                         (simp_tac (put_simpset HOL_basic_ss ctxt''
   65.82                            addsimps [inductive_forall_def']
   65.83 @@ -431,9 +432,10 @@
   65.84                 in resolve_tac ctxt' final' 1 end) context 1])
   65.85                   (prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems'')))
   65.86          in
   65.87 -          cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
   65.88 +          cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt' [conjE] 1) THEN
   65.89            REPEAT (REPEAT (resolve_tac ctxt' [conjI, impI] 1) THEN
   65.90 -            etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
   65.91 +            eresolve_tac ctxt' [impE] 1 THEN
   65.92 +            assume_tac ctxt' 1 THEN REPEAT (eresolve_tac ctxt' @{thms allE_Nil} 1) THEN
   65.93              asm_full_simp_tac ctxt 1)
   65.94          end) |>
   65.95          fresh_postprocess ctxt' |>
    66.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Jul 18 20:53:05 2015 +0200
    66.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Jul 18 20:54:56 2015 +0200
    66.3 @@ -218,7 +218,7 @@
    66.4  fun perm_compose_tac ctxt i = 
    66.5    ("analysing permutation compositions on the lhs",
    66.6     fn st => EVERY
    66.7 -     [rtac trans i,
    66.8 +     [resolve_tac ctxt [trans] i,
    66.9        asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
   66.10        asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
   66.11  
   66.12 @@ -230,14 +230,15 @@
   66.13  (*     pi o f = rhs                           *)  
   66.14  (* is transformed to                          *)
   66.15  (*     %x. pi o (f ((rev pi) o x)) = rhs      *)
   66.16 -fun unfold_perm_fun_def_tac i =
   66.17 +fun unfold_perm_fun_def_tac ctxt i =
   66.18      ("unfolding of permutations on functions", 
   66.19 -      rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
   66.20 +      resolve_tac ctxt [perm_fun_def RS meta_eq_to_obj_eq RS trans] i)
   66.21  
   66.22  (* applies the ext-rule such that      *)
   66.23  (*                                     *)
   66.24  (*    f = g   goes to  /\x. f x = g x  *)
   66.25 -fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i);
   66.26 +fun ext_fun_tac ctxt i =
   66.27 +  ("extensionality expansion of functions", resolve_tac ctxt @{thms ext} i);
   66.28  
   66.29  
   66.30  (* perm_extend_simp_tac_i is perm_simp plus additional tactics        *)
   66.31 @@ -248,13 +249,14 @@
   66.32    let fun perm_extend_simp_tac_aux tactical ctxt n = 
   66.33            if n=0 then K all_tac
   66.34            else DETERM o 
   66.35 -               (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i),
   66.36 -                       fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
   66.37 -                       fn i => tactical ctxt (perm_compose_tac ctxt i),
   66.38 -                       fn i => tactical ctxt (apply_cong_tac ctxt i), 
   66.39 -                       fn i => tactical ctxt (unfold_perm_fun_def_tac i),
   66.40 -                       fn i => tactical ctxt (ext_fun_tac i)]
   66.41 -                      THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
   66.42 +               (FIRST'
   66.43 +                 [fn i => tactical ctxt ("splitting conjunctions on the rhs", resolve_tac ctxt [conjI] i),
   66.44 +                  fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
   66.45 +                  fn i => tactical ctxt (perm_compose_tac ctxt i),
   66.46 +                  fn i => tactical ctxt (apply_cong_tac ctxt i), 
   66.47 +                  fn i => tactical ctxt (unfold_perm_fun_def_tac ctxt i),
   66.48 +                  fn i => tactical ctxt (ext_fun_tac ctxt i)]
   66.49 +                THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
   66.50    in perm_extend_simp_tac_aux tactical ctxt 10 end;
   66.51  
   66.52  
   66.53 @@ -266,10 +268,10 @@
   66.54       val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
   66.55    in
   66.56        EVERY [tactical ctxt ("unfolding of supports   ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
   66.57 -             tactical ctxt ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
   66.58 -             tactical ctxt ("geting rid of the imps  ", rtac impI i),
   66.59 -             tactical ctxt ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
   66.60 -             tactical ctxt ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )]
   66.61 +             tactical ctxt ("stripping of foralls    ", REPEAT_DETERM (resolve_tac ctxt [allI] i)),
   66.62 +             tactical ctxt ("geting rid of the imps  ", resolve_tac ctxt [impI] i),
   66.63 +             tactical ctxt ("eliminating conjuncts   ", REPEAT_DETERM (eresolve_tac ctxt [conjE] i)),
   66.64 +             tactical ctxt ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i)]
   66.65    end;
   66.66  
   66.67  
    67.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sat Jul 18 20:53:05 2015 +0200
    67.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sat Jul 18 20:54:56 2015 +0200
    67.3 @@ -58,12 +58,12 @@
    67.4      val mypifree = Thm.global_cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
    67.5      val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
    67.6    in
    67.7 -    EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}),
    67.8 -            tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
    67.9 -            tactic ctxt ("solve with orig_thm", etac orig_thm),
   67.10 +    EVERY1 [tactic ctxt ("iffI applied", resolve_tac ctxt @{thms iffI}),
   67.11 +            tactic ctxt ("remove pi with perm_boolE", dresolve_tac ctxt @{thms perm_boolE}),
   67.12 +            tactic ctxt ("solve with orig_thm", eresolve_tac ctxt [orig_thm]),
   67.13              tactic ctxt ("applies orig_thm instantiated with rev pi",
   67.14 -                       dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
   67.15 -            tactic ctxt ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
   67.16 +                       dresolve_tac ctxt [Drule.cterm_instantiate [(mypi,mypifree)] orig_thm]),
   67.17 +            tactic ctxt ("getting rid of the pi on the right", resolve_tac ctxt @{thms perm_boolI}),
   67.18              tactic ctxt ("getting rid of all remaining perms",
   67.19                         full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))]
   67.20    end;
    68.1 --- a/src/HOL/Prolog/prolog.ML	Sat Jul 18 20:53:05 2015 +0200
    68.2 +++ b/src/HOL/Prolog/prolog.ML	Sat Jul 18 20:54:56 2015 +0200
    68.3 @@ -74,7 +74,7 @@
    68.4  (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
    68.5                                    resolve_tac (maps atomizeD prems) 1);
    68.6    -- is nice, but cannot instantiate unknowns in the assumptions *)
    68.7 -val hyp_resolve_tac = SUBGOAL (fn (subgoal, i) =>
    68.8 +fun hyp_resolve_tac ctxt = SUBGOAL (fn (subgoal, i) =>
    68.9    let
   68.10          fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
   68.11          |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   68.12 @@ -91,9 +91,9 @@
   68.13          val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
   68.14          fun drot_tac k i = DETERM (rotate_tac k i);
   68.15          fun spec_tac 0 i = all_tac
   68.16 -        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
   68.17 +        |   spec_tac k i = EVERY' [dresolve_tac ctxt [spec], drot_tac ~1, spec_tac (k-1)] i;
   68.18          fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
   68.19 -                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
   68.20 +                      [DETERM o (eresolve_tac ctxt [all_dupE]), drot_tac ~2, spec_tac (k-1)] i;
   68.21          fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
   68.22          |   same_head k (s$_)         (t$_)         = same_head k s t
   68.23          |   same_head k (Bound i)     (Bound j)     = i = j + k
   68.24 @@ -101,10 +101,10 @@
   68.25          fun mapn f n []      = []
   68.26          |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
   68.27          fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
   68.28 -                if same_head k t concl
   68.29 -                then dup_spec_tac k i THEN
   68.30 -                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
   68.31 -                else no_tac);
   68.32 +          if same_head k t concl
   68.33 +          then dup_spec_tac k i THEN
   68.34 +               (if arrow then eresolve_tac ctxt [mp] i THEN drot_tac (~n) i else assume_tac ctxt i)
   68.35 +          else no_tac);
   68.36          val ptacs = mapn (fn n => fn t =>
   68.37                            pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   68.38    in Library.foldl (op APPEND) (no_tac, ptacs) end);
   68.39 @@ -112,16 +112,16 @@
   68.40  fun ptac ctxt prog = let
   68.41    val proga = maps (atomizeD ctxt) prog         (* atomize the prog *)
   68.42    in    (REPEAT_DETERM1 o FIRST' [
   68.43 -                rtac TrueI,                     (* "True" *)
   68.44 -                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
   68.45 -                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
   68.46 -                rtac exI,                       (* "P x ==> ? x. P x" *)
   68.47 -                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
   68.48 +                resolve_tac ctxt [TrueI],                     (* "True" *)
   68.49 +                resolve_tac ctxt [conjI],                     (* "[| P; Q |] ==> P & Q" *)
   68.50 +                resolve_tac ctxt [allI],                      (* "(!!x. P x) ==> ! x. P x" *)
   68.51 +                resolve_tac ctxt [exI],                       (* "P x ==> ? x. P x" *)
   68.52 +                resolve_tac ctxt [impI] THEN'                 (* "(P ==> Q) ==> P --> Q" *)
   68.53                    asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN'    (* atomize the asms *)
   68.54 -                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
   68.55 +                  (REPEAT_DETERM o (eresolve_tac ctxt [conjE]))        (* split the asms *)
   68.56                  ])
   68.57          ORELSE' resolve_tac ctxt [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
   68.58 -        ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac)
   68.59 +        ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac ctxt)
   68.60                   THEN' (fn _ => check_HOHH_tac2))
   68.61  end;
   68.62  
    69.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sat Jul 18 20:53:05 2015 +0200
    69.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sat Jul 18 20:54:56 2015 +0200
    69.3 @@ -540,7 +540,7 @@
    69.4      (fn i =>
    69.5        EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
    69.6               assume_tac ctxt i,
    69.7 -             etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
    69.8 +             eresolve_tac ctxt [conjE] i, REPEAT (hyp_subst_tac ctxt i)]))
    69.9  *}
   69.10  
   69.11  text{*The @{text "(no_asm)"} attribute is essential, since it retains
    70.1 --- a/src/HOL/SET_Protocol/Event_SET.thy	Sat Jul 18 20:53:05 2015 +0200
    70.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy	Sat Jul 18 20:54:56 2015 +0200
    70.3 @@ -183,7 +183,7 @@
    70.4  ML
    70.5  {*
    70.6  fun analz_mono_contra_tac ctxt = 
    70.7 -  rtac @{thm analz_impI} THEN' 
    70.8 +  resolve_tac ctxt @{thms analz_impI} THEN' 
    70.9    REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
   70.10    THEN' mp_tac ctxt
   70.11  *}
    71.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Jul 18 20:53:05 2015 +0200
    71.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Jul 18 20:54:56 2015 +0200
    71.3 @@ -206,22 +206,22 @@
    71.4      val UNIV_eq = Goal.prove lthy [] []
    71.5        (HOLogic.mk_Trueprop (HOLogic.mk_eq
    71.6           (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
    71.7 -      (fn _ =>
    71.8 -         rtac @{thm subset_antisym} 1 THEN
    71.9 -         rtac @{thm subsetI} 1 THEN
   71.10 -         Old_Datatype_Aux.exh_tac lthy (K (#exhaust (BNF_LFP_Compat.the_info
   71.11 -           (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
   71.12 -         ALLGOALS (asm_full_simp_tac lthy));
   71.13 +      (fn {context = ctxt, ...} =>
   71.14 +         resolve_tac ctxt @{thms subset_antisym} 1 THEN
   71.15 +         resolve_tac ctxt @{thms subsetI} 1 THEN
   71.16 +         Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info
   71.17 +           (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
   71.18 +         ALLGOALS (asm_full_simp_tac ctxt));
   71.19  
   71.20      val finite_UNIV = Goal.prove lthy [] []
   71.21        (HOLogic.mk_Trueprop (Const (@{const_name finite},
   71.22           HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
   71.23 -      (fn _ => simp_tac (lthy addsimps [UNIV_eq]) 1);
   71.24 +      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
   71.25  
   71.26      val card_UNIV = Goal.prove lthy [] []
   71.27        (HOLogic.mk_Trueprop (HOLogic.mk_eq
   71.28           (card, HOLogic.mk_number HOLogic.natT k)))
   71.29 -      (fn _ => simp_tac (lthy addsimps [UNIV_eq]) 1);
   71.30 +      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
   71.31  
   71.32      val range_pos = Goal.prove lthy [] []
   71.33        (HOLogic.mk_Trueprop (HOLogic.mk_eq
   71.34 @@ -232,20 +232,20 @@
   71.35              HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
   71.36                HOLogic.mk_number HOLogic.intT 0 $
   71.37                (@{term int} $ card))))
   71.38 -      (fn _ =>
   71.39 -         simp_tac (lthy addsimps [card_UNIV]) 1 THEN
   71.40 -         simp_tac (lthy addsimps [UNIV_eq, def1]) 1 THEN
   71.41 -         rtac @{thm subset_antisym} 1 THEN
   71.42 -         simp_tac lthy 1 THEN
   71.43 -         rtac @{thm subsetI} 1 THEN
   71.44 -         asm_full_simp_tac (lthy addsimps @{thms interval_expand}
   71.45 +      (fn {context = ctxt, ...} =>
   71.46 +         simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
   71.47 +         simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
   71.48 +         resolve_tac ctxt @{thms subset_antisym} 1 THEN
   71.49 +         simp_tac ctxt 1 THEN
   71.50 +         resolve_tac ctxt @{thms subsetI} 1 THEN
   71.51 +         asm_full_simp_tac (ctxt addsimps @{thms interval_expand}
   71.52             delsimps @{thms atLeastLessThan_iff}) 1);
   71.53  
   71.54      val lthy' =
   71.55        Class.prove_instantiation_instance (fn ctxt =>
   71.56          Class.intro_classes_tac ctxt [] THEN
   71.57 -        rtac finite_UNIV 1 THEN
   71.58 -        rtac range_pos 1 THEN
   71.59 +        resolve_tac ctxt [finite_UNIV] 1 THEN
   71.60 +        resolve_tac ctxt [range_pos] 1 THEN
   71.61          simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN
   71.62          simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy;
   71.63  
   71.64 @@ -254,23 +254,24 @@
   71.65          val n = HOLogic.mk_number HOLogic.intT i;
   71.66          val th = Goal.prove lthy' [] []
   71.67            (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))
   71.68 -          (fn _ => simp_tac (lthy' addsimps [def1]) 1);
   71.69 +          (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1);
   71.70          val th' = Goal.prove lthy' [] []
   71.71            (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))
   71.72 -          (fn _ =>
   71.73 -             rtac (@{thm inj_pos} RS @{thm injD}) 1 THEN
   71.74 -             simp_tac (lthy' addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
   71.75 +          (fn {context = ctxt, ...} =>
   71.76 +             resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN
   71.77 +             simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
   71.78        in (th, th') end) cs);
   71.79  
   71.80      val first_el = Goal.prove lthy' [] []
   71.81        (HOLogic.mk_Trueprop (HOLogic.mk_eq
   71.82           (Const (@{const_name first_el}, T), hd cs)))
   71.83 -      (fn _ => simp_tac (lthy' addsimps [@{thm first_el_def}, hd val_eqs]) 1);
   71.84 +      (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
   71.85  
   71.86      val last_el = Goal.prove lthy' [] []
   71.87        (HOLogic.mk_Trueprop (HOLogic.mk_eq
   71.88           (Const (@{const_name last_el}, T), List.last cs)))
   71.89 -      (fn _ => simp_tac (lthy' addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
   71.90 +      (fn {context = ctxt, ...} =>
   71.91 +        simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
   71.92    in
   71.93      lthy' |>
   71.94      Local_Theory.note
    72.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sat Jul 18 20:53:05 2015 +0200
    72.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sat Jul 18 20:54:56 2015 +0200
    72.3 @@ -345,7 +345,7 @@
    72.4        Const (@{const_name Trueprop}, _) $
    72.5            (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)) =>
    72.6          (case get_fst_success (neq_x_y ctxt x y) names of
    72.7 -          SOME neq => rtac neq i
    72.8 +          SOME neq => resolve_tac ctxt [neq] i
    72.9          | NONE => no_tac)
   72.10      | _ => no_tac))
   72.11  
    73.1 --- a/src/HOL/Statespace/state_fun.ML	Sat Jul 18 20:53:05 2015 +0200
    73.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Jul 18 20:54:56 2015 +0200
    73.3 @@ -248,7 +248,7 @@
    73.4                    val eq1 =
    73.5                      Goal.prove ctxt0 [] []
    73.6                        (Logic.list_all (vars, Logic.mk_equals (trm, trm')))
    73.7 -                      (fn _ => rtac meta_ext 1 THEN simp_tac ctxt1 1);
    73.8 +                      (fn _ => resolve_tac ctxt0 [meta_ext] 1 THEN simp_tac ctxt1 1);
    73.9                    val eq2 = Simplifier.asm_full_rewrite ctxt2 (Thm.dest_equals_rhs (Thm.cprop_of eq1));
   73.10                  in SOME (Thm.transitive eq1 eq2) end
   73.11              | _ => NONE)
    74.1 --- a/src/HOL/Statespace/state_space.ML	Sat Jul 18 20:53:05 2015 +0200
    74.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Jul 18 20:54:56 2015 +0200
    74.3 @@ -204,7 +204,7 @@
    74.4        (Const (@{const_name Not}, _) $
    74.5          (Const (@{const_name HOL.eq}, _) $ (x as Free _) $ (y as Free _))) =>
    74.6        (case neq_x_y ctxt x y of
    74.7 -        SOME neq => rtac neq i
    74.8 +        SOME neq => resolve_tac ctxt [neq] i
    74.9        | NONE => no_tac)
   74.10    | _ => no_tac));
   74.11  
   74.12 @@ -222,7 +222,7 @@
   74.13        let
   74.14          val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name;
   74.15          val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal;
   74.16 -      in rtac rule i end);
   74.17 +      in resolve_tac ctxt [rule] i end);
   74.18  
   74.19      fun tac ctxt =
   74.20        Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt);
    75.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Jul 18 20:53:05 2015 +0200
    75.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Jul 18 20:54:56 2015 +0200
    75.3 @@ -227,7 +227,7 @@
    75.4    val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
    75.5    val fast_solver = mk_solver "fast_solver" (fn ctxt =>
    75.6      if Config.get ctxt config_fast_solver
    75.7 -    then assume_tac ctxt ORELSE' (etac notE)
    75.8 +    then assume_tac ctxt ORELSE' (eresolve_tac ctxt [notE])
    75.9      else K no_tac);
   75.10  \<close>
   75.11  
   75.12 @@ -797,7 +797,7 @@
   75.13  ML \<open>
   75.14  fun split_idle_tac ctxt =
   75.15    SELECT_GOAL
   75.16 -   (TRY (rtac @{thm actionI} 1) THEN
   75.17 +   (TRY (resolve_tac ctxt @{thms actionI} 1) THEN
   75.18      Induct_Tacs.case_tac ctxt "(s,t) \<Turnstile> unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN
   75.19      rewrite_goals_tac ctxt @{thms action_rews} THEN
   75.20      forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
    76.1 --- a/src/HOL/TLA/TLA.thy	Sat Jul 18 20:53:05 2015 +0200
    76.2 +++ b/src/HOL/TLA/TLA.thy	Sat Jul 18 20:54:56 2015 +0200
    76.3 @@ -284,23 +284,24 @@
    76.4  lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
    76.5  
    76.6  ML \<open>
    76.7 -fun merge_box_tac i =
    76.8 -   REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
    76.9 +fun merge_box_tac ctxt i =
   76.10 +   REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE} i, assume_tac ctxt i,
   76.11 +    eresolve_tac ctxt @{thms box_thin} i])
   76.12  
   76.13  fun merge_temp_box_tac ctxt i =
   76.14 -  REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
   76.15 +  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_temp} i, assume_tac ctxt i,
   76.16      Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i])
   76.17  
   76.18  fun merge_stp_box_tac ctxt i =
   76.19 -  REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
   76.20 +  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_stp} i, assume_tac ctxt i,
   76.21      Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i])
   76.22  
   76.23  fun merge_act_box_tac ctxt i =
   76.24 -  REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
   76.25 +  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_act} i, assume_tac ctxt i,
   76.26      Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
   76.27  \<close>
   76.28  
   76.29 -method_setup merge_box = \<open>Scan.succeed (K (SIMPLE_METHOD' merge_box_tac))\<close>
   76.30 +method_setup merge_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_box_tac)\<close>
   76.31  method_setup merge_temp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\<close>
   76.32  method_setup merge_stp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\<close>
   76.33  method_setup merge_act_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\<close>
   76.34 @@ -577,9 +578,9 @@
   76.35    SELECT_GOAL
   76.36      (EVERY
   76.37       [auto_tac ctxt,
   76.38 -      TRY (merge_box_tac 1),
   76.39 -      rtac (temp_use ctxt @{thm INV1}) 1, (* fail if the goal is not a box *)
   76.40 -      TRYALL (etac @{thm Stable})]);
   76.41 +      TRY (merge_box_tac ctxt 1),
   76.42 +      resolve_tac ctxt [temp_use ctxt @{thm INV1}] 1, (* fail if the goal is not a box *)
   76.43 +      TRYALL (eresolve_tac ctxt @{thms Stable})]);
   76.44  
   76.45  (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
   76.46     in simple cases it may be able to handle goals like \<turnstile> MyProg \<longrightarrow> \<box>Inv.
    77.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sat Jul 18 20:53:05 2015 +0200
    77.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sat Jul 18 20:54:56 2015 +0200
    77.3 @@ -975,9 +975,9 @@
    77.4              raise SKELETON (*FIXME or classify it as a Caboose: TRY (HEADGOAL atac) *)
    77.5            else
    77.6              case hd skel of
    77.7 -                Assumed => TRY (HEADGOAL atac) THEN rest (tl skel) memo
    77.8 -              | Caboose => TRY (HEADGOAL atac)
    77.9 -              | Unconjoin => rtac @{thm conjI} 1 THEN rest (tl skel) memo
   77.10 +                Assumed => TRY (HEADGOAL (assume_tac ctxt)) THEN rest (tl skel) memo
   77.11 +              | Caboose => TRY (HEADGOAL (assume_tac ctxt))
   77.12 +              | Unconjoin => resolve_tac ctxt @{thms conjI} 1 THEN rest (tl skel) memo
   77.13                | Split (split_node, solved_node, antes) =>
   77.14                    let
   77.15                      val split_fmla = node_info (#meta pannot) #fmla split_node
   77.16 @@ -993,13 +993,13 @@
   77.17                      val split_thm =
   77.18                        simulate_split ctxt split_fmla minor_prems_assumps conclusion
   77.19                    in
   77.20 -                    rtac split_thm 1 THEN rest (tl skel) memo
   77.21 +                    resolve_tac ctxt [split_thm] 1 THEN rest (tl skel) memo
   77.22                    end
   77.23                | Step s =>
   77.24                    let
   77.25 -                    val (tac, memo') = tac_and_memo s memo
   77.26 +                    val (th, memo') = tac_and_memo s memo
   77.27                    in
   77.28 -                    rtac tac 1 THEN rest (tl skel) memo'
   77.29 +                    resolve_tac ctxt [th] 1 THEN rest (tl skel) memo'
   77.30                    end
   77.31                | Definition n =>
   77.32                    let
   77.33 @@ -1008,7 +1008,7 @@
   77.34                            NONE => error ("Did not find definition: " ^ n)
   77.35                          | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
   77.36                    in
   77.37 -                    rtac def_thm 1 THEN rest (tl skel) memo
   77.38 +                    resolve_tac ctxt [def_thm] 1 THEN rest (tl skel) memo
   77.39                    end
   77.40                | Axiom n =>
   77.41                    let
   77.42 @@ -1017,7 +1017,7 @@
   77.43                            NONE => error ("Did not find axiom: " ^ n)
   77.44                          | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
   77.45                    in
   77.46 -                    rtac ax_thm 1 THEN rest (tl skel) memo
   77.47 +                    resolve_tac ctxt [ax_thm] 1 THEN rest (tl skel) memo
   77.48                    end
   77.49                | _ => raise SKELETON
   77.50        in tactic st end
   77.51 @@ -1065,7 +1065,7 @@
   77.52               let
   77.53                 fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string)
   77.54                 val reconstructed_inference = thm ctxt'
   77.55 -               fun rec_inf_tac st = HEADGOAL (rtac (thm ctxt')) st
   77.56 +               fun rec_inf_tac st = HEADGOAL (resolve_tac ctxt' [thm ctxt']) st
   77.57               in (reconstructed_inference,
   77.58                   rec_inf_tac)
   77.59               end)
   77.60 @@ -1088,17 +1088,17 @@
   77.61                  (hd skel,
   77.62                   Thm.prop_of @{thm asm_rl}
   77.63                   |> SOME,
   77.64 -                 SOME (@{thm asm_rl}, TRY (HEADGOAL atac))) :: rest memo ctxt
   77.65 +                 SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt)))) :: rest memo ctxt
   77.66              | Caboose =>
   77.67                  [(Caboose,
   77.68                    Thm.prop_of @{thm asm_rl}
   77.69                    |> SOME,
   77.70 -                  SOME (@{thm asm_rl}, TRY (HEADGOAL atac)))]
   77.71 +                  SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt))))]
   77.72              | Unconjoin =>
   77.73                  (hd skel,
   77.74                   Thm.prop_of @{thm conjI}
   77.75                   |> SOME,
   77.76 -                 SOME (@{thm conjI}, rtac @{thm conjI} 1)) :: rest memo ctxt
   77.77 +                 SOME (@{thm conjI}, resolve_tac ctxt @{thms conjI} 1)) :: rest memo ctxt
   77.78              | Split (split_node, solved_node, antes) =>
   77.79                  let
   77.80                    val split_fmla = node_info (#meta pannot) #fmla split_node
   77.81 @@ -1117,7 +1117,7 @@
   77.82                    (hd skel,
   77.83                     Thm.prop_of split_thm
   77.84                     |> SOME,
   77.85 -                   SOME (split_thm, rtac split_thm 1)) :: rest memo ctxt
   77.86 +                   SOME (split_thm, resolve_tac ctxt [split_thm] 1)) :: rest memo ctxt
   77.87                  end
   77.88              | Step node =>
   77.89                  let
   77.90 @@ -1180,7 +1180,7 @@
   77.91                    (hd skel,
   77.92                     Thm.prop_of (def_thm thy)
   77.93                     |> SOME,
   77.94 -                   SOME (def_thm thy, HEADGOAL (rtac (def_thm thy)))) :: rest memo ctxt
   77.95 +                   SOME (def_thm thy, HEADGOAL (resolve_tac ctxt [def_thm thy]))) :: rest memo ctxt
   77.96                  end
   77.97              | Axiom n =>
   77.98                  let
   77.99 @@ -1192,7 +1192,7 @@
  77.100                    (hd skel,
  77.101                     Thm.prop_of ax_thm
  77.102                     |> SOME,
  77.103 -                   SOME (ax_thm, rtac ax_thm 1)) :: rest memo ctxt
  77.104 +                   SOME (ax_thm, resolve_tac ctxt [ax_thm] 1)) :: rest memo ctxt
  77.105                  end
  77.106        end
  77.107  
  77.108 @@ -1216,7 +1216,7 @@
  77.109           TPTP_Proof.is_inference_called "solved_all_splits"
  77.110            (the last_inference_info)
  77.111          then (@{thm asm_rl}, all_tac)
  77.112 -        else (solved_all_splits, TRY (rtac solved_all_splits 1))
  77.113 +        else (solved_all_splits, TRY (resolve_tac ctxt [solved_all_splits] 1))
  77.114        end
  77.115  in
  77.116    (*Build a tactic from a skeleton. This is naive because it uses the naive skeleton.
  77.117 @@ -1226,8 +1226,8 @@
  77.118      let
  77.119        val thy = Proof_Context.theory_of ctxt
  77.120      in
  77.121 -      rtac @{thm ccontr} 1
  77.122 -      THEN dtac neg_eq_false 1
  77.123 +      resolve_tac ctxt @{thms ccontr} 1
  77.124 +      THEN dresolve_tac ctxt [neg_eq_false] 1
  77.125        THEN (sas_if_needed_tac ctxt prob_name |> #2)
  77.126        THEN skel_to_naive_tactic ctxt prover_tac prob_name
  77.127         (make_skeleton ctxt
  77.128 @@ -1241,9 +1241,9 @@
  77.129        val thy = Proof_Context.theory_of ctxt
  77.130      in
  77.131        (Synth_step "ccontr", Thm.prop_of @{thm ccontr} |> SOME,
  77.132 -       SOME (@{thm ccontr}, rtac @{thm ccontr} 1)) ::
  77.133 +       SOME (@{thm ccontr}, resolve_tac ctxt @{thms ccontr} 1)) ::
  77.134        (Synth_step "neg_eq_false", Thm.prop_of neg_eq_false |> SOME,
  77.135 -       SOME (neg_eq_false, dtac neg_eq_false 1)) ::
  77.136 +       SOME (neg_eq_false, dresolve_tac ctxt [neg_eq_false] 1)) ::
  77.137        (Synth_step "sas_if_needed_tac", Thm.prop_of @{thm asm_rl} (*FIXME *) |> SOME,
  77.138         SOME (sas_if_needed_tac ctxt prob_name)) ::
  77.139        skel_to_naive_tactic_dbg prover_tac ctxt prob_name
    78.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Jul 18 20:53:05 2015 +0200
    78.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Jul 18 20:54:56 2015 +0200
    78.3 @@ -282,13 +282,13 @@
    78.4           val thm = Goal.prove ctxt [] []
    78.5             (Logic.mk_implies (hyp_clause, new_hyp))
    78.6             (fn _ =>
    78.7 -              (REPEAT_DETERM (HEADGOAL (rtac @{thm allI})))
    78.8 +              (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI})))
    78.9                THEN (REPEAT_DETERM
   78.10                      (HEADGOAL
   78.11                       (nominal_inst_parametermatch_tac ctxt @{thm allE})))
   78.12 -              THEN HEADGOAL atac)
   78.13 +              THEN HEADGOAL (assume_tac ctxt))
   78.14        in
   78.15 -        dtac thm i st
   78.16 +        dresolve_tac ctxt [thm] i st
   78.17        end
   78.18      end
   78.19  *}
   78.20 @@ -305,8 +305,8 @@
   78.21    (TPTP_Reconstruct.remove_polarity true t; true)
   78.22    handle TPTP_Reconstruct.UNPOLARISED _ => false
   78.23  
   78.24 -val polarise_subgoal_hyps =
   78.25 -  COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dtac @{thm polarise})
   78.26 +fun polarise_subgoal_hyps ctxt =
   78.27 +  COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dresolve_tac ctxt @{thms polarise})
   78.28  *}
   78.29  
   78.30  lemma simp_meta [rule_format]:
   78.31 @@ -336,10 +336,10 @@
   78.32  
   78.33  lemma solved_all_splits: "False = True \<Longrightarrow> False" by simp
   78.34  ML {*
   78.35 -val solved_all_splits_tac =
   78.36 -  TRY (etac @{thm conjE} 1)
   78.37 -  THEN rtac @{thm solved_all_splits} 1
   78.38 -  THEN atac 1
   78.39 +fun solved_all_splits_tac ctxt =
   78.40 +  TRY (eresolve_tac ctxt @{thms conjE} 1)
   78.41 +  THEN resolve_tac ctxt @{thms solved_all_splits} 1
   78.42 +  THEN assume_tac ctxt 1
   78.43  *}
   78.44  
   78.45  lemma lots_of_logic_expansions_meta [rule_format]:
   78.46 @@ -433,10 +433,10 @@
   78.47  
   78.48      fun instantiate_tac vars =
   78.49        instantiate_vars ctxt vars
   78.50 -      THEN (HEADGOAL atac)
   78.51 +      THEN (HEADGOAL (assume_tac ctxt))
   78.52    in
   78.53      HEADGOAL (canonicalise_qtfr_order ctxt)
   78.54 -    THEN (REPEAT_DETERM (HEADGOAL (rtac @{thm allI})))
   78.55 +    THEN (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI})))
   78.56      THEN REPEAT_DETERM (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE}))
   78.57      (*now only the variable to instantiate should be left*)
   78.58      THEN FIRST (map instantiate_tac ordered_instances)
   78.59 @@ -470,8 +470,8 @@
   78.60    let
   78.61      val default_tac =
   78.62        (TRY o CHANGED o (rewrite_goal_tac ctxt @{thms prop_normalise}))
   78.63 -      THEN' rtac @{thm notI}
   78.64 -      THEN' (REPEAT_DETERM o etac @{thm conjE})
   78.65 +      THEN' resolve_tac ctxt @{thms notI}
   78.66 +      THEN' (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE})
   78.67        THEN' (TRY o (expander_animal ctxt))
   78.68    in
   78.69      default_tac ORELSE' resolve_tac ctxt @{thms flip}
   78.70 @@ -646,8 +646,6 @@
   78.71  ML {*
   78.72  fun forall_neg_tac candidate_consts ctxt i = fn st =>
   78.73    let
   78.74 -    val thy = Proof_Context.theory_of ctxt
   78.75 -
   78.76      val gls =
   78.77        Thm.prop_of st
   78.78        |> Logic.strip_horn
   78.79 @@ -749,7 +747,7 @@
   78.80            else
   78.81              raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
   78.82    in
   78.83 -    rtac (Drule.export_without_context thm) i st
   78.84 +    resolve_tac ctxt [Drule.export_without_context thm] i st
   78.85    end
   78.86    handle SKOLEM_DEF _ => no_tac st
   78.87  *}
   78.88 @@ -960,12 +958,12 @@
   78.89  ML {*
   78.90  fun new_skolem_tac ctxt consts_candidates =
   78.91    let
   78.92 -    fun tec thm =
   78.93 -      dtac thm
   78.94 +    fun tac thm =
   78.95 +      dresolve_tac ctxt [thm]
   78.96        THEN' instantiate_skols ctxt consts_candidates
   78.97    in
   78.98      if null consts_candidates then K no_tac
   78.99 -    else FIRST' (map tec @{thms lift_exists})
  78.100 +    else FIRST' (map tac @{thms lift_exists})
  78.101    end
  78.102  *}
  78.103  
  78.104 @@ -1142,7 +1140,7 @@
  78.105              those free variables into logical variables.*)
  78.106            |> Thm.forall_intr_frees
  78.107            |> Drule.export_without_context
  78.108 -      in dtac rule i st end
  78.109 +      in dresolve_tac ctxt [rule] i st end
  78.110        handle NO_GOALS => no_tac st
  78.111  
  78.112      fun closure tac =
  78.113 @@ -1151,10 +1149,10 @@
  78.114        SOLVE o (tac THEN' (batter_tac ctxt ORELSE' assume_tac ctxt))
  78.115      val search_tac =
  78.116        ASAP
  78.117 -        (rtac @{thm disjI1} APPEND' rtac @{thm disjI2})
  78.118 +        (resolve_tac ctxt @{thms disjI1} APPEND' resolve_tac ctxt @{thms disjI2})
  78.119          (FIRST' (map closure
  78.120                    [dresolve_tac ctxt @{thms dec_commut_eq},
  78.121 -                   dtac @{thm dec_commut_disj},
  78.122 +                   dresolve_tac ctxt @{thms dec_commut_disj},
  78.123                     elim_tac]))
  78.124    in
  78.125      (CHANGED o search_tac) i st
  78.126 @@ -1306,14 +1304,15 @@
  78.127                v
  78.128    \<lbrakk>A = True; B = False\<rbrakk> \<Longrightarrow> R
  78.129  *)
  78.130 -fun weak_conj_tac drule =
  78.131 -  dtac drule THEN' (REPEAT_DETERM o etac @{thm conjE})
  78.132 +fun weak_conj_tac ctxt drule =
  78.133 +  dresolve_tac ctxt [drule] THEN'
  78.134 +  (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE})
  78.135  *}
  78.136  
  78.137  ML {*
  78.138 -val uncurry_lit_neg_tac =
  78.139 -  dtac @{lemma "(A \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> C) = False" by auto}
  78.140 -  #> REPEAT_DETERM
  78.141 +fun uncurry_lit_neg_tac ctxt =
  78.142 +  REPEAT_DETERM o
  78.143 +    dresolve_tac ctxt [@{lemma "(A \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> C) = False" by auto}]
  78.144  *}
  78.145  
  78.146  ML {*
  78.147 @@ -1326,10 +1325,10 @@
  78.148              let
  78.149                val rule = mk_standard_cnf ctxt kind arity;
  78.150              in
  78.151 -              (weak_conj_tac rule THEN' atac) i st
  78.152 +              (weak_conj_tac ctxt rule THEN' assume_tac ctxt) i st
  78.153              end
  78.154    in
  78.155 -    (uncurry_lit_neg_tac
  78.156 +    (uncurry_lit_neg_tac ctxt
  78.157       THEN' TPTP_Reconstruct_Library.reassociate_conjs_tac ctxt
  78.158       THEN' core_tactic) i st
  78.159    end
  78.160 @@ -1473,13 +1472,13 @@
  78.161  (*use as elim rule to remove premises*)
  78.162  lemma insa_prems: "\<lbrakk>Q; P\<rbrakk> \<Longrightarrow> P" by auto
  78.163  ML {*
  78.164 -fun cleanup_skolem_defs feats =
  78.165 +fun cleanup_skolem_defs ctxt feats =
  78.166    let
  78.167      (*remove hypotheses from skolem defs,
  78.168       after testing that they look like skolem defs*)
  78.169      val dehypothesise_skolem_defs =
  78.170        COND' (SOME #> TERMPRED (fn _ => true) conc_is_skolem_def)
  78.171 -        (REPEAT_DETERM o etac @{thm insa_prems})
  78.172 +        (REPEAT_DETERM o eresolve_tac ctxt @{thms insa_prems})
  78.173          (K no_tac)
  78.174    in
  78.175      if can_feature (CleanUp [RemoveHypothesesFromSkolemDefs]) feats then
  78.176 @@ -1497,11 +1496,11 @@
  78.177  
  78.178  ML {*
  78.179  (*given a goal state, indicates the skolem constants committed-to in it (i.e. appearing in LHS of a skolem definition)*)
  78.180 -val which_skolem_concs_used = fn st =>
  78.181 +fun which_skolem_concs_used ctxt = fn st =>
  78.182    let
  78.183      val feats = [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]]
  78.184      val scrubup_tac =
  78.185 -      cleanup_skolem_defs feats
  78.186 +      cleanup_skolem_defs ctxt feats
  78.187        THEN remove_duplicates_tac feats
  78.188    in
  78.189      scrubup_tac st
  78.190 @@ -1547,7 +1546,7 @@
  78.191  (*predicate over the type of the leading quantified variable*)
  78.192  
  78.193  ML {*
  78.194 -val extcnf_forall_special_pos_tac =
  78.195 +fun extcnf_forall_special_pos_tac ctxt =
  78.196    let
  78.197      val bool =
  78.198        ["True", "False"]
  78.199 @@ -1555,16 +1554,16 @@
  78.200      val bool_to_bool =
  78.201        ["% _ . True", "% _ . False", "% x . x", "Not"]
  78.202  
  78.203 -    val tecs =
  78.204 +    val tacs =
  78.205        map (fn t_s =>  (* FIXME proper context!? *)
  78.206         Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] [] @{thm allE}
  78.207 -       THEN' atac)
  78.208 +       THEN' assume_tac ctxt)
  78.209    in
  78.210 -    (TRY o etac @{thm forall_pos_lift})
  78.211 -    THEN' (atac
  78.212 +    (TRY o eresolve_tac ctxt @{thms forall_pos_lift})
  78.213 +    THEN' (assume_tac ctxt
  78.214             ORELSE' FIRST'
  78.215              (*FIXME could check the type of the leading quantified variable, instead of trying everything*)
  78.216 -            (tecs (bool @ bool_to_bool)))
  78.217 +            (tacs (bool @ bool_to_bool)))
  78.218    end
  78.219  *}
  78.220  
  78.221 @@ -1573,9 +1572,9 @@
  78.222  
  78.223  lemma efq: "[|A = True; A = False|] ==> R" by auto
  78.224  ML {*
  78.225 -val efq_tac =
  78.226 -  (etac @{thm efq} THEN' atac)
  78.227 -  ORELSE' atac
  78.228 +fun efq_tac ctxt =
  78.229 +  (eresolve_tac ctxt @{thms efq} THEN' assume_tac ctxt)
  78.230 +  ORELSE' assume_tac ctxt
  78.231  *}
  78.232  
  78.233  ML {*
  78.234 @@ -1586,13 +1585,13 @@
  78.235        consisting of a Skolem definition*)
  78.236      fun extcnf_combined_tac' ctxt i = fn st =>
  78.237        let
  78.238 -        val skolem_consts_used_so_far = which_skolem_concs_used st
  78.239 +        val skolem_consts_used_so_far = which_skolem_concs_used ctxt st
  78.240          val consts_diff' = subtract (op =) skolem_consts_used_so_far consts_diff
  78.241  
  78.242          fun feat_to_tac feat =
  78.243            case feat of
  78.244 -              Close_Branch => trace_tac' ctxt "mark: closer" efq_tac
  78.245 -            | ConjI => trace_tac' ctxt "mark: conjI" (rtac @{thm conjI})
  78.246 +              Close_Branch => trace_tac' ctxt "mark: closer" (efq_tac ctxt)
  78.247 +            | ConjI => trace_tac' ctxt "mark: conjI" (resolve_tac ctxt @{thms conjI})
  78.248              | King_Cong => trace_tac' ctxt "mark: expander_animal" (expander_animal ctxt)
  78.249              | Break_Hypotheses => trace_tac' ctxt "mark: break_hypotheses" (break_hypotheses_tac ctxt)
  78.250              | RemoveRedundantQuantifications => K all_tac
  78.251 @@ -1603,28 +1602,28 @@
  78.252                   (REPEAT_DETERM o remove_redundant_quantification_in_lit)
  78.253  *)
  78.254  
  78.255 -            | Assumption => atac
  78.256 +            | Assumption => assume_tac ctxt
  78.257  (*FIXME both Existential_Free and Existential_Var run same code*)
  78.258              | Existential_Free => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
  78.259              | Existential_Var => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
  78.260              | Universal => trace_tac' ctxt "mark: forall_pos" (forall_tac ctxt feats)
  78.261 -            | Not_pos => trace_tac' ctxt "mark: not_pos" (dtac @{thm leo2_rules(9)})
  78.262 -            | Not_neg => trace_tac' ctxt "mark: not_neg" (dtac @{thm leo2_rules(10)})
  78.263 -            | Or_pos => trace_tac' ctxt "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
  78.264 -            | Or_neg => trace_tac' ctxt "mark: or_neg" (dtac @{thm leo2_rules(7)})
  78.265 +            | Not_pos => trace_tac' ctxt "mark: not_pos" (dresolve_tac ctxt @{thms leo2_rules(9)})
  78.266 +            | Not_neg => trace_tac' ctxt "mark: not_neg" (dresolve_tac ctxt @{thms leo2_rules(10)})
  78.267 +            | Or_pos => trace_tac' ctxt "mark: or_pos" (dresolve_tac ctxt @{thms leo2_rules(5)}) (*could add (6) for negated conjunction*)
  78.268 +            | Or_neg => trace_tac' ctxt "mark: or_neg" (dresolve_tac ctxt @{thms leo2_rules(7)})
  78.269              | Equal_pos => trace_tac' ctxt "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
  78.270              | Equal_neg => trace_tac' ctxt "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
  78.271              | Donkey_Cong => trace_tac' ctxt "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
  78.272  
  78.273 -            | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dtac @{thm extuni_bool2})
  78.274 -            | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dtac @{thm extuni_bool1})
  78.275 -            | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
  78.276 -            | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
  78.277 +            | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dresolve_tac ctxt @{thms extuni_bool2})
  78.278 +            | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dresolve_tac ctxt @{thms extuni_bool1})
  78.279 +            | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (eresolve_tac ctxt @{thms extuni_triv})
  78.280 +            | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (eresolve_tac ctxt @{thms extuni_triv})
  78.281              | Extuni_Dec => trace_tac' ctxt "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
  78.282 -            | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
  78.283 -            | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dtac @{thm extuni_func})
  78.284 +            | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (assume_tac ctxt ORELSE' asm_full_simp_tac ctxt)
  78.285 +            | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dresolve_tac ctxt @{thms extuni_func})
  78.286              | Polarity_switch => trace_tac' ctxt "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
  78.287 -            | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" extcnf_forall_special_pos_tac
  78.288 +            | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" (extcnf_forall_special_pos_tac ctxt)
  78.289  
  78.290          val core_tac =
  78.291            get_loop_feats feats
  78.292 @@ -1668,8 +1667,8 @@
  78.293     @{const_name Pure.imp}]
  78.294  
  78.295  fun strip_qtfrs_tac ctxt =
  78.296 -  REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))
  78.297 -  THEN REPEAT_DETERM (HEADGOAL (etac @{thm exE}))
  78.298 +  REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI}))
  78.299 +  THEN REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms exE}))
  78.300    THEN HEADGOAL (canonicalise_qtfr_order ctxt)
  78.301    THEN
  78.302      ((REPEAT (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE})))
  78.303 @@ -1846,7 +1845,7 @@
  78.304        then we should be left with skolem definitions:
  78.305          absorb them as axioms into the theory.*)
  78.306      val cleanup =
  78.307 -      cleanup_skolem_defs feats
  78.308 +      cleanup_skolem_defs ctxt feats
  78.309        THEN remove_duplicates_tac feats
  78.310        THEN (if can_feature AbsorbSkolemDefs feats then
  78.311                ALLGOALS (absorb_skolem_def ctxt prob_name_opt)
  78.312 @@ -1868,9 +1867,9 @@
  78.313          can be simply eliminated -- they're redundant*)
  78.314        (*FIXME instead of just using allE, instantiate to a silly
  78.315           term, to remove opportunities for unification.*)
  78.316 -      THEN (REPEAT_DETERM (etac @{thm allE} 1))
  78.317 +      THEN (REPEAT_DETERM (eresolve_tac ctxt @{thms allE} 1))
  78.318  
  78.319 -      THEN (REPEAT_DETERM (rtac @{thm allI} 1))
  78.320 +      THEN (REPEAT_DETERM (resolve_tac ctxt @{thms allI} 1))
  78.321  
  78.322        THEN (if have_loop_feats then
  78.323                REPEAT (CHANGED
  78.324 @@ -1914,32 +1913,33 @@
  78.325        discharged.
  78.326       *)
  78.327      val kill_meta_eqs_tac =
  78.328 -      dtac @{thm un_meta_polarise}
  78.329 -      THEN' rtac @{thm meta_polarise}
  78.330 -      THEN' (REPEAT_DETERM o (etac @{thm conjE}))
  78.331 -      THEN' (REPEAT_DETERM o (rtac @{thm conjI} ORELSE' atac))
  78.332 +      dresolve_tac ctxt @{thms un_meta_polarise}
  78.333 +      THEN' resolve_tac ctxt @{thms meta_polarise}
  78.334 +      THEN' (REPEAT_DETERM o (eresolve_tac ctxt @{thms conjE}))
  78.335 +      THEN' (REPEAT_DETERM o (resolve_tac ctxt @{thms conjI} ORELSE' assume_tac ctxt))
  78.336  
  78.337      val continue_reducing_tac =
  78.338 -      rtac @{thm meta_eq_to_obj_eq} 1
  78.339 +      resolve_tac ctxt @{thms meta_eq_to_obj_eq} 1
  78.340        THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
  78.341 -      THEN TRY (polarise_subgoal_hyps 1) (*no need to REPEAT_DETERM here, since there should only be one hypothesis*)
  78.342 -      THEN TRY (dtac @{thm eq_reflection} 1)
  78.343 +      THEN TRY (polarise_subgoal_hyps ctxt 1) (*no need to REPEAT_DETERM here, since there should only be one hypothesis*)
  78.344 +      THEN TRY (dresolve_tac ctxt @{thms eq_reflection} 1)
  78.345        THEN (TRY ((CHANGED o rewrite_goal_tac ctxt
  78.346                (@{thm expand_iff} :: @{thms simp_meta})) 1))
  78.347 -      THEN HEADGOAL (rtac @{thm reflexive}
  78.348 -                     ORELSE' atac
  78.349 +      THEN HEADGOAL (resolve_tac ctxt @{thms reflexive}
  78.350 +                     ORELSE' assume_tac ctxt
  78.351                       ORELSE' kill_meta_eqs_tac)
  78.352  
  78.353      val tactic =
  78.354 -      (rtac @{thm polarise} 1 THEN atac 1)
  78.355 +      (resolve_tac ctxt @{thms polarise} 1 THEN assume_tac ctxt 1)
  78.356        ORELSE
  78.357 -        (REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1)
  78.358 +        (REPEAT_DETERM (eresolve_tac ctxt @{thms conjE} 1 THEN
  78.359 +          eresolve_tac ctxt @{thms drop_first_hypothesis} 1)
  78.360           THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
  78.361           THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
  78.362           THEN (TRY ((CHANGED o rewrite_goal_tac ctxt @{thms simp_meta}) 1))
  78.363           THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
  78.364           THEN
  78.365 -           (HEADGOAL atac
  78.366 +           (HEADGOAL (assume_tac ctxt)
  78.367             ORELSE
  78.368              (unfold_tac ctxt depends_on_defs
  78.369               THEN IF_UNSOLVED continue_reducing_tac)))
  78.370 @@ -2117,12 +2117,12 @@
  78.371          *)
  78.372      | "copy" =>
  78.373           HEADGOAL
  78.374 -          (atac
  78.375 +          (assume_tac ctxt
  78.376             ORELSE'
  78.377 -              (rtac @{thm polarise}
  78.378 -               THEN' atac))
  78.379 +              (resolve_tac ctxt @{thms polarise}
  78.380 +               THEN' assume_tac ctxt))
  78.381      | "polarity_switch" => nonfull_extcnf_combined_tac [Polarity_switch]
  78.382 -    | "solved_all_splits" => solved_all_splits_tac
  78.383 +    | "solved_all_splits" => solved_all_splits_tac ctxt
  78.384      | "extcnf_not_pos" => nonfull_extcnf_combined_tac [Not_pos]
  78.385      | "extcnf_forall_pos" => nonfull_extcnf_combined_tac [Universal]
  78.386      | "negate_conjecture" => fail ctxt "Should not handle negate_conjecture here"
  78.387 @@ -2138,7 +2138,7 @@
  78.388      | "extuni_bool2" => nonfull_extcnf_combined_tac [Extuni_Bool2]
  78.389      | "extuni_bool1" => nonfull_extcnf_combined_tac [Extuni_Bool1]
  78.390      | "extuni_dec" =>
  78.391 -        HEADGOAL atac
  78.392 +        HEADGOAL (assume_tac ctxt)
  78.393          ORELSE nonfull_extcnf_combined_tac [Extuni_Dec]
  78.394      | "extuni_bind" => nonfull_extcnf_combined_tac [Extuni_Bind]
  78.395      | "extuni_triv" => nonfull_extcnf_combined_tac [Extuni_Triv]
  78.396 @@ -2161,7 +2161,7 @@
  78.397      | "split_preprocessing" =>
  78.398           (REPEAT (HEADGOAL (split_simp_tac ctxt)))
  78.399           THEN TRY (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion))
  78.400 -         THEN HEADGOAL atac
  78.401 +         THEN HEADGOAL (assume_tac ctxt)
  78.402  
  78.403      (*FIXME some of these could eventually be handled specially*)
  78.404      | "fac_restr" => default_tac
    79.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Sat Jul 18 20:53:05 2015 +0200
    79.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Sat Jul 18 20:54:56 2015 +0200
    79.3 @@ -712,7 +712,7 @@
    79.4  fun rename_client_map_tac ctxt =
    79.5    EVERY [
    79.6      simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
    79.7 -    rtac @{thm guarantees_PLam_I} 1,
    79.8 +    resolve_tac ctxt @{thms guarantees_PLam_I} 1,
    79.9      assume_tac ctxt 2,
   79.10           (*preserves: routine reasoning*)
   79.11      asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2,
   79.12 @@ -899,9 +899,9 @@
   79.13  text{*safety (1), step 4 (final result!) *}
   79.14  theorem System_safety: "System : system_safety"
   79.15    apply (unfold system_safety_def)
   79.16 -  apply (tactic {* rtac (Always_Int_rule [@{thm System_sum_bounded},
   79.17 +  apply (tactic {* resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded},
   79.18      @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS
   79.19 -    @{thm Always_weaken}) 1 *})
   79.20 +    @{thm Always_weaken}] 1 *})
   79.21    apply auto
   79.22    apply (rule setsum_fun_mono [THEN order_trans])
   79.23    apply (drule_tac [2] order_trans)
   79.24 @@ -942,8 +942,8 @@
   79.25  lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
   79.26                            ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}"
   79.27    apply (auto simp add: Collect_all_imp_eq)
   79.28 -  apply (tactic {* rtac (Always_Int_rule [@{thm Always_allocAsk_le_ask},
   79.29 -    @{thm System_Bounded_ask}] RS @{thm Always_weaken}) 1 *})
   79.30 +  apply (tactic {* resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask},
   79.31 +    @{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1 *})
   79.32    apply (auto dest: set_mono)
   79.33    done
   79.34  
    80.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Jul 18 20:53:05 2015 +0200
    80.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Jul 18 20:54:56 2015 +0200
    80.3 @@ -104,11 +104,11 @@
    80.4  fun ns_constrains_tac ctxt i =
    80.5    SELECT_GOAL
    80.6      (EVERY
    80.7 -     [REPEAT (etac @{thm Always_ConstrainsI} 1),
    80.8 +     [REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1),
    80.9        REPEAT (resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1),
   80.10 -      rtac @{thm ns_constrainsI} 1,
   80.11 +      resolve_tac ctxt @{thms ns_constrainsI} 1,
   80.12        full_simp_tac ctxt 1,
   80.13 -      REPEAT (FIRSTGOAL (etac disjE)),
   80.14 +      REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
   80.15        ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])),
   80.16        REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)),
   80.17        ALLGOALS (asm_simp_tac ctxt)]) i;
   80.18 @@ -116,10 +116,10 @@
   80.19  (*Tactic for proving secrecy theorems*)
   80.20  fun ns_induct_tac ctxt =
   80.21    (SELECT_GOAL o EVERY)
   80.22 -     [rtac @{thm AlwaysI} 1,
   80.23 +     [resolve_tac ctxt @{thms AlwaysI} 1,
   80.24        force_tac ctxt 1,
   80.25        (*"reachable" gets in here*)
   80.26 -      rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
   80.27 +      resolve_tac ctxt [@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}] 1,
   80.28        ns_constrains_tac ctxt 1];
   80.29  *}
   80.30  
    81.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Sat Jul 18 20:53:05 2015 +0200
    81.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Sat Jul 18 20:54:56 2015 +0200
    81.3 @@ -7,7 +7,9 @@
    81.4  
    81.5  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
    81.6  fun Always_Int_tac ctxt =
    81.7 -  dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}
    81.8 +  dresolve_tac ctxt @{thms Always_Int_I} THEN'
    81.9 +  assume_tac ctxt THEN'
   81.10 +  eresolve_tac ctxt @{thms Always_thin}
   81.11  
   81.12  (*Combines a list of invariance THEOREMS into one.*)
   81.13  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
   81.14 @@ -19,16 +21,16 @@
   81.15      (EVERY
   81.16       [REPEAT (Always_Int_tac ctxt 1),
   81.17        (*reduce the fancy safety properties to "constrains"*)
   81.18 -      REPEAT (etac @{thm Always_ConstrainsI} 1
   81.19 +      REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
   81.20                ORELSE
   81.21                resolve_tac ctxt [@{thm StableI}, @{thm stableI},
   81.22                             @{thm constrains_imp_Constrains}] 1),
   81.23        (*for safety, the totalize operator can be ignored*)
   81.24        simp_tac (put_simpset HOL_ss ctxt
   81.25          addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
   81.26 -      rtac @{thm constrainsI} 1,
   81.27 +      resolve_tac ctxt @{thms constrainsI} 1,
   81.28        full_simp_tac ctxt 1,
   81.29 -      REPEAT (FIRSTGOAL (etac disjE)),
   81.30 +      REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
   81.31        ALLGOALS (clarify_tac ctxt),
   81.32        ALLGOALS (asm_full_simp_tac ctxt)]) i;
   81.33  
   81.34 @@ -37,7 +39,7 @@
   81.35    SELECT_GOAL
   81.36      (EVERY
   81.37       [REPEAT (Always_Int_tac ctxt 1),
   81.38 -      etac @{thm Always_LeadsTo_Basis} 1
   81.39 +      eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
   81.40            ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   81.41            REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
   81.42                              @{thm EnsuresI}, @{thm ensuresI}] 1),
    82.1 --- a/src/HOL/Word/Word.thy	Sat Jul 18 20:53:05 2015 +0200
    82.2 +++ b/src/HOL/Word/Word.thy	Sat Jul 18 20:54:56 2015 +0200
    82.3 @@ -1562,8 +1562,8 @@
    82.4            |> fold Simplifier.add_cong @{thms power_False_cong})),
    82.5        rewrite_goals_tac ctxt @{thms word_size}, 
    82.6        ALLGOALS  (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
    82.7 -                         REPEAT (etac conjE n) THEN
    82.8 -                         REPEAT (dtac @{thm word_of_int_inverse} n 
    82.9 +                         REPEAT (eresolve_tac ctxt [conjE] n) THEN
   82.10 +                         REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n 
   82.11                                   THEN assume_tac ctxt n 
   82.12                                   THEN assume_tac ctxt n)),
   82.13        TRYALL arith_tac' ]
   82.14 @@ -2063,9 +2063,9 @@
   82.15            |> fold Splitter.add_split @{thms unat_splits}
   82.16            |> fold Simplifier.add_cong @{thms power_False_cong})),
   82.17        rewrite_goals_tac ctxt @{thms word_size}, 
   82.18 -      ALLGOALS  (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN      
   82.19 -                         REPEAT (etac conjE n) THEN
   82.20 -                         REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
   82.21 +      ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
   82.22 +                         REPEAT (eresolve_tac ctxt [conjE] n) THEN
   82.23 +                         REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)),
   82.24        TRYALL arith_tac' ] 
   82.25    end
   82.26  
    83.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Sat Jul 18 20:53:05 2015 +0200
    83.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Jul 18 20:54:56 2015 +0200
    83.3 @@ -33,7 +33,7 @@
    83.4      [OF \<open>x = y\<close>]}.\<close>
    83.5  
    83.6    have "x = y"
    83.7 -    by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
    83.8 +    by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
    83.9  end
   83.10  
   83.11  
   83.12 @@ -230,10 +230,10 @@
   83.13  \<close>
   83.14  
   83.15  lemma "A \<and> B \<longrightarrow> B \<and> A"
   83.16 -  apply (ml_tactic \<open>rtac @{thm impI} 1\<close>)
   83.17 -  apply (ml_tactic \<open>etac @{thm conjE} 1\<close>)
   83.18 -  apply (ml_tactic \<open>rtac @{thm conjI} 1\<close>)
   83.19 -  apply (ml_tactic \<open>ALLGOALS atac\<close>)
   83.20 +  apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>)
   83.21 +  apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>)
   83.22 +  apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
   83.23 +  apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>)
   83.24    done
   83.25  
   83.26  lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
   83.27 @@ -251,14 +251,17 @@
   83.28  \<close>
   83.29  
   83.30  lemma "A \<and> B \<longrightarrow> B \<and> A"
   83.31 -  apply \<open>rtac @{thm impI} 1\<close>
   83.32 -  apply \<open>etac @{thm conjE} 1\<close>
   83.33 -  apply \<open>rtac @{thm conjI} 1\<close>
   83.34 -  apply \<open>ALLGOALS atac\<close>
   83.35 +  apply \<open>resolve_tac @{context} @{thms impI} 1\<close>
   83.36 +  apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close>
   83.37 +  apply \<open>resolve_tac @{context} @{thms conjI} 1\<close>
   83.38 +  apply \<open>ALLGOALS (assume_tac @{context})\<close>
   83.39    done
   83.40  
   83.41  lemma "A \<and> B \<longrightarrow> B \<and> A"
   83.42 -  by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
   83.43 +  by (\<open>resolve_tac @{context} @{thms impI} 1\<close>,
   83.44 +    \<open>eresolve_tac @{context} @{thms conjE} 1\<close>,
   83.45 +    \<open>resolve_tac @{context} @{thms conjI} 1\<close>,
   83.46 +    \<open>assume_tac @{context} 1\<close>+)
   83.47  
   83.48  
   83.49  subsection \<open>ML syntax\<close>
    84.1 --- a/src/HOL/ex/Iff_Oracle.thy	Sat Jul 18 20:53:05 2015 +0200
    84.2 +++ b/src/HOL/ex/Iff_Oracle.thy	Sat Jul 18 20:54:56 2015 +0200
    84.3 @@ -58,7 +58,7 @@
    84.4  method_setup iff =
    84.5    \<open>Scan.lift Parse.nat >> (fn n => fn ctxt =>
    84.6      SIMPLE_METHOD
    84.7 -      (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
    84.8 +      (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)])
    84.9          handle Fail _ => no_tac))\<close>
   84.10  
   84.11  
    85.1 --- a/src/HOL/ex/Meson_Test.thy	Sat Jul 18 20:53:05 2015 +0200
    85.2 +++ b/src/HOL/ex/Meson_Test.thy	Sat Jul 18 20:54:56 2015 +0200
    85.3 @@ -29,7 +29,7 @@
    85.4      val nnf25 = Meson.make_nnf ctxt prem25;
    85.5      val xsko25 = Meson.skolemize ctxt nnf25;
    85.6    *}
    85.7 -  apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *})
    85.8 +  apply (tactic {* cut_tac xsko25 1 THEN REPEAT (eresolve_tac @{context} [exE] 1) *})
    85.9    ML_val {*
   85.10      val ctxt = @{context};
   85.11      val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
   85.12 @@ -39,7 +39,7 @@
   85.13  
   85.14      val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
   85.15      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   85.16 -      rtac go25 1 THEN
   85.17 +      resolve_tac ctxt' [go25] 1 THEN
   85.18        Meson.depth_prolog_tac ctxt' horns25);
   85.19    *}
   85.20    oops
   85.21 @@ -53,7 +53,7 @@
   85.22      val nnf26 = Meson.make_nnf ctxt prem26;
   85.23      val xsko26 = Meson.skolemize ctxt nnf26;
   85.24    *}
   85.25 -  apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *})
   85.26 +  apply (tactic {* cut_tac xsko26 1 THEN REPEAT (eresolve_tac @{context} [exE] 1) *})
   85.27    ML_val {*
   85.28      val ctxt = @{context};
   85.29      val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
   85.30 @@ -65,7 +65,7 @@
   85.31  
   85.32      val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
   85.33      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   85.34 -      rtac go26 1 THEN
   85.35 +      resolve_tac ctxt' [go26] 1 THEN
   85.36        Meson.depth_prolog_tac ctxt' horns26);  (*7 ms*)
   85.37      (*Proof is of length 107!!*)
   85.38    *}
   85.39 @@ -80,7 +80,7 @@
   85.40      val nnf43 = Meson.make_nnf ctxt prem43;
   85.41      val xsko43 = Meson.skolemize ctxt nnf43;
   85.42    *}
   85.43 -  apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *})
   85.44 +  apply (tactic {* cut_tac xsko43 1 THEN REPEAT (eresolve_tac @{context} [exE] 1) *})
   85.45    ML_val {*
   85.46      val ctxt = @{context};
   85.47      val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
   85.48 @@ -92,7 +92,7 @@
   85.49  
   85.50      val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
   85.51      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   85.52 -      rtac go43 1 THEN
   85.53 +      resolve_tac ctxt' [go43] 1 THEN
   85.54        Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43);   (*7ms*)
   85.55      *}
   85.56    oops
    86.1 --- a/src/Provers/Arith/assoc_fold.ML	Sat Jul 18 20:53:05 2015 +0200
    86.2 +++ b/src/Provers/Arith/assoc_fold.ML	Sat Jul 18 20:54:56 2015 +0200
    86.3 @@ -44,8 +44,10 @@
    86.4      val (lits, others) = sift_terms plus (lhs, ([],[]))
    86.5      val _ = length lits < 2 andalso raise Assoc_fail (*we can't reduce the number of terms*)
    86.6      val rhs = plus $ mk_sum plus lits $ mk_sum plus others
    86.7 -    val th = Goal.prove ctxt [] [] (Logic.mk_equals (lhs, rhs))
    86.8 -      (fn _ => rtac Data.eq_reflection 1 THEN simp_tac (put_simpset Data.assoc_ss ctxt) 1)
    86.9 +    val th =
   86.10 +      Goal.prove ctxt [] [] (Logic.mk_equals (lhs, rhs)) (fn _ =>
   86.11 +        resolve_tac ctxt [Data.eq_reflection] 1 THEN
   86.12 +        simp_tac (put_simpset Data.assoc_ss ctxt) 1)
   86.13    in SOME th end handle Assoc_fail => NONE;
   86.14  
   86.15  end;
    87.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Sat Jul 18 20:53:05 2015 +0200
    87.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Sat Jul 18 20:54:56 2015 +0200
    87.3 @@ -72,7 +72,7 @@
    87.4    in
    87.5      Option.map (export o Data.simplify_meta_eq ctxt)
    87.6        (Data.prove_conv
    87.7 -         [Data.trans_tac ctxt reshape, rtac Data.cancel 1,
    87.8 +         [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.cancel] 1,
    87.9            Data.numeral_simp_tac ctxt] ctxt prems (t', rhs))
   87.10    end
   87.11    (* FIXME avoid handling of generic exceptions *)
    88.1 --- a/src/Sequents/LK.thy	Sat Jul 18 20:53:05 2015 +0200
    88.2 +++ b/src/Sequents/LK.thy	Sat Jul 18 20:54:56 2015 +0200
    88.3 @@ -178,7 +178,7 @@
    88.4    apply (lem p1)
    88.5    apply safe
    88.6     apply (tactic {*
    88.7 -     REPEAT (rtac @{thm cut} 1 THEN
    88.8 +     REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
    88.9         DEPTH_SOLVE_1
   88.10           (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
   88.11             Cla.safe_tac @{context} 1) *})
   88.12 @@ -191,7 +191,7 @@
   88.13    apply (lem p1)
   88.14    apply safe
   88.15     apply (tactic {*
   88.16 -     REPEAT (rtac @{thm cut} 1 THEN
   88.17 +     REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
   88.18         DEPTH_SOLVE_1
   88.19           (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
   88.20             Cla.safe_tac @{context} 1) *})
    89.1 --- a/src/Sequents/LK0.thy	Sat Jul 18 20:53:05 2015 +0200
    89.2 +++ b/src/Sequents/LK0.thy	Sat Jul 18 20:54:56 2015 +0200
    89.3 @@ -154,12 +154,12 @@
    89.4  (*Cut and thin, replacing the right-side formula*)
    89.5  fun cutR_tac ctxt s i =
    89.6    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
    89.7 -  rtac @{thm thinR} i
    89.8 +  resolve_tac ctxt @{thms thinR} i
    89.9  
   89.10  (*Cut and thin, replacing the left-side formula*)
   89.11  fun cutL_tac ctxt s i =
   89.12    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
   89.13 -  rtac @{thm thinL} (i + 1)
   89.14 +  resolve_tac ctxt @{thms thinL} (i + 1)
   89.15  *}
   89.16  
   89.17  
   89.18 @@ -244,11 +244,11 @@
   89.19    {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt))) *}
   89.20  
   89.21  method_setup lem = {*
   89.22 -  Attrib.thm >> (fn th => fn _ =>
   89.23 +  Attrib.thm >> (fn th => fn ctxt =>
   89.24      SIMPLE_METHOD' (fn i =>
   89.25 -      rtac (@{thm thinR} RS @{thm cut}) i THEN
   89.26 -      REPEAT (rtac @{thm thinL} i) THEN
   89.27 -      rtac th i))
   89.28 +      resolve_tac ctxt [@{thm thinR} RS @{thm cut}] i THEN
   89.29 +      REPEAT (resolve_tac ctxt @{thms thinL} i) THEN
   89.30 +      resolve_tac ctxt [th] i))
   89.31  *}
   89.32  
   89.33  
    90.1 --- a/src/ZF/UNITY/Constrains.thy	Sat Jul 18 20:53:05 2015 +0200
    90.2 +++ b/src/ZF/UNITY/Constrains.thy	Sat Jul 18 20:54:56 2015 +0200
    90.3 @@ -460,7 +460,9 @@
    90.4  {*
    90.5  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
    90.6  fun Always_Int_tac ctxt =
    90.7 -  dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin};
    90.8 +  dresolve_tac ctxt @{thms Always_Int_I} THEN'
    90.9 +  assume_tac ctxt THEN'
   90.10 +  eresolve_tac ctxt @{thms Always_thin};
   90.11  
   90.12  (*Combines a list of invariance THEOREMS into one.*)
   90.13  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
   90.14 @@ -470,26 +472,28 @@
   90.15  fun constrains_tac ctxt =
   90.16     SELECT_GOAL
   90.17        (EVERY [REPEAT (Always_Int_tac ctxt 1),
   90.18 -              REPEAT (etac @{thm Always_ConstrainsI} 1
   90.19 +              REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
   90.20                        ORELSE
   90.21                        resolve_tac ctxt [@{thm StableI}, @{thm stableI},
   90.22                                     @{thm constrains_imp_Constrains}] 1),
   90.23 -              rtac @{thm constrainsI} 1,
   90.24 +              resolve_tac ctxt @{thms constrainsI} 1,
   90.25                (* Three subgoals *)
   90.26                rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
   90.27                REPEAT (force_tac ctxt 2),
   90.28                full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 1,
   90.29                ALLGOALS (clarify_tac ctxt),
   90.30 -              REPEAT (FIRSTGOAL (etac @{thm disjE})),
   90.31 +              REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})),
   90.32                ALLGOALS (clarify_tac ctxt),
   90.33 -              REPEAT (FIRSTGOAL (etac @{thm disjE})),
   90.34 +              REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})),
   90.35                ALLGOALS (clarify_tac ctxt),
   90.36                ALLGOALS (asm_full_simp_tac ctxt),
   90.37                ALLGOALS (clarify_tac ctxt)]);
   90.38  
   90.39  (*For proving invariants*)
   90.40  fun always_tac ctxt i =
   90.41 -    rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
   90.42 +  resolve_tac ctxt @{thms AlwaysI} i THEN
   90.43 +  force_tac ctxt i
   90.44 +  THEN constrains_tac ctxt i;
   90.45  *}
   90.46  
   90.47  method_setup safety = {*
    91.1 --- a/src/ZF/UNITY/SubstAx.thy	Sat Jul 18 20:53:05 2015 +0200
    91.2 +++ b/src/ZF/UNITY/SubstAx.thy	Sat Jul 18 20:54:56 2015 +0200
    91.3 @@ -353,7 +353,7 @@
    91.4  fun ensures_tac ctxt sact =
    91.5    SELECT_GOAL
    91.6      (EVERY [REPEAT (Always_Int_tac ctxt 1),
    91.7 -            etac @{thm Always_LeadsTo_Basis} 1
    91.8 +            eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
    91.9                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   91.10                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
   91.11                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
   91.12 @@ -364,10 +364,11 @@
   91.13                 (*simplify the command's domain*)
   91.14              simp_tac (ctxt addsimps [@{thm domain_def}]) 3,
   91.15              (* proving the domain part *)
   91.16 -           clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4,
   91.17 -           rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
   91.18 -           asm_full_simp_tac ctxt 3, rtac @{thm conjI} 3, simp_tac ctxt 4,
   91.19 -           REPEAT (rtac @{thm state_update_type} 3),
   91.20 +           clarify_tac ctxt 3,
   91.21 +           dresolve_tac ctxt @{thms swap} 3, force_tac ctxt 4,
   91.22 +           resolve_tac ctxt @{thms ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
   91.23 +           asm_full_simp_tac ctxt 3, resolve_tac ctxt @{thms conjI} 3, simp_tac ctxt 4,
   91.24 +           REPEAT (resolve_tac ctxt @{thms state_update_type} 3),
   91.25             constrains_tac ctxt 1,
   91.26             ALLGOALS (clarify_tac ctxt),
   91.27             ALLGOALS (asm_full_simp_tac (ctxt addsimps [@{thm st_set_def}])),