prefer tactics with explicit context;
authorwenzelm
Sat Jul 18 20:47:08 2015 +0200 (2015-07-18)
changeset 60752b48830b670a1
parent 60751 83f04804696c
child 60753 80ca4a065a48
prefer tactics with explicit context;
src/HOL/Filter.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Old_SMT/old_smt_solver.ML
src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/bnf_lfp_countable.ML
src/HOL/Library/old_recdef.ML
src/HOL/List.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/SMT/conj_disj_perm.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/z3_replay.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record.ML
src/HOL/Tools/reification.ML
     1.1 --- a/src/HOL/Filter.thy	Sat Jul 18 20:37:16 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Sat Jul 18 20:47:08 2015 +0200
     1.3 @@ -250,7 +250,7 @@
     1.4            (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
     1.5        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
     1.6      in
     1.7 -      CASES cases (rtac raw_elim_thm i)
     1.8 +      CASES cases (resolve_tac ctxt [raw_elim_thm] i)
     1.9      end)
    1.10  *}
    1.11  
     2.1 --- a/src/HOL/Library/Countable.thy	Sat Jul 18 20:37:16 2015 +0200
     2.2 +++ b/src/HOL/Library/Countable.thy	Sat Jul 18 20:47:08 2015 +0200
     2.3 @@ -186,10 +186,10 @@
     2.4          val rules = @{thms finite_item.intros}
     2.5        in
     2.6          SOLVED' (fn i => EVERY
     2.7 -          [rtac @{thm countable_datatype} i,
     2.8 -           rtac typedef_thm i,
     2.9 -           etac induct_thm' i,
    2.10 -           REPEAT (resolve_tac ctxt rules i ORELSE atac i)]) 1
    2.11 +          [resolve_tac ctxt @{thms countable_datatype} i,
    2.12 +           resolve_tac ctxt [typedef_thm] i,
    2.13 +           eresolve_tac ctxt [induct_thm'] i,
    2.14 +           REPEAT (resolve_tac ctxt rules i ORELSE assume_tac ctxt i)]) 1
    2.15        end)
    2.16  \<close>
    2.17  
     3.1 --- a/src/HOL/Library/Multiset.thy	Sat Jul 18 20:37:16 2015 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Sat Jul 18 20:47:08 2015 +0200
     3.3 @@ -1898,23 +1898,25 @@
     3.4              Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
     3.5                    mk_mset T [x] $ mk_mset T xs
     3.6  
     3.7 -    fun mset_member_tac m i =
     3.8 +    fun mset_member_tac ctxt m i =
     3.9        if m <= 0 then
    3.10 -        rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i
    3.11 +        resolve_tac ctxt @{thms multi_member_this} i ORELSE
    3.12 +        resolve_tac ctxt @{thms multi_member_last} i
    3.13        else
    3.14 -        rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i
    3.15 -
    3.16 -    val mset_nonempty_tac =
    3.17 -      rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
    3.18 +        resolve_tac ctxt @{thms multi_member_skip} i THEN mset_member_tac ctxt (m - 1) i
    3.19 +
    3.20 +    fun mset_nonempty_tac ctxt =
    3.21 +      resolve_tac ctxt @{thms nonempty_plus} ORELSE'
    3.22 +      resolve_tac ctxt @{thms nonempty_single}
    3.23  
    3.24      fun regroup_munion_conv ctxt =
    3.25        Function_Lib.regroup_conv ctxt @{const_abbrev Mempty} @{const_name plus}
    3.26          (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
    3.27  
    3.28 -    fun unfold_pwleq_tac i =
    3.29 -      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
    3.30 -        ORELSE (rtac @{thm pw_leq_lstep} i)
    3.31 -        ORELSE (rtac @{thm pw_leq_empty} i)
    3.32 +    fun unfold_pwleq_tac ctxt i =
    3.33 +      (resolve_tac ctxt @{thms pw_leq_step} i THEN (fn st => unfold_pwleq_tac ctxt (i + 1) st))
    3.34 +        ORELSE (resolve_tac ctxt @{thms pw_leq_lstep} i)
    3.35 +        ORELSE (resolve_tac ctxt @{thms pw_leq_empty} i)
    3.36  
    3.37      val set_mset_simps = [@{thm set_mset_empty}, @{thm set_mset_single}, @{thm set_mset_union},
    3.38                          @{thm Un_insert_left}, @{thm Un_empty_left}]
    3.39 @@ -1925,7 +1927,7 @@
    3.40        mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
    3.41        mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_mset_simps,
    3.42        smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
    3.43 -      reduction_pair= @{thm ms_reduction_pair}
    3.44 +      reduction_pair = @{thm ms_reduction_pair}
    3.45      })
    3.46    end
    3.47  \<close>
     4.1 --- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Sat Jul 18 20:37:16 2015 +0200
     4.2 +++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Sat Jul 18 20:47:08 2015 +0200
     4.3 @@ -355,14 +355,14 @@
     4.4    fun tag_rules thms = map_index (apsnd (pair NONE)) thms
     4.5    fun tag_prems thms = map (pair ~1 o pair NONE) thms
     4.6  
     4.7 -  fun resolve (SOME thm) = rtac thm 1
     4.8 -    | resolve NONE = no_tac
     4.9 +  fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1
    4.10 +    | resolve _ NONE = no_tac
    4.11  
    4.12    fun tac prove ctxt rules =
    4.13      CONVERSION (Old_SMT_Normalize.atomize_conv ctxt)
    4.14 -    THEN' rtac @{thm ccontr}
    4.15 -    THEN' SUBPROOF (fn {context, prems, ...} =>
    4.16 -      resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
    4.17 +    THEN' resolve_tac ctxt @{thms ccontr}
    4.18 +    THEN' SUBPROOF (fn {context = ctxt', prems, ...} =>
    4.19 +      resolve ctxt' (prove ctxt' (tag_rules rules @ tag_prems prems))) ctxt
    4.20  in
    4.21  
    4.22  val smt_tac = tac safe_solve
     5.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sat Jul 18 20:37:16 2015 +0200
     5.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sat Jul 18 20:47:08 2015 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4  fun prove_ite ctxt =
     5.5    Old_Z3_Proof_Tools.by_tac ctxt (
     5.6      CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
     5.7 -    THEN' rtac @{thm refl})
     5.8 +    THEN' resolve_tac ctxt @{thms refl})
     5.9  
    5.10  
    5.11  
    5.12 @@ -71,7 +71,7 @@
    5.13      val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)]
    5.14    in
    5.15      Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
    5.16 -    |> apply (rtac @{thm injI})
    5.17 +    |> apply (resolve_tac ctxt' @{thms injI})
    5.18      |> apply (Tactic.solve_tac ctxt' [rule, rule RS @{thm sym}])
    5.19      |> Goal.norm_result ctxt' o Goal.finish ctxt'
    5.20      |> singleton (Variable.export ctxt' ctxt)
    5.21 @@ -81,7 +81,7 @@
    5.22    Old_Z3_Proof_Tools.by_tac ctxt (
    5.23      CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
    5.24      THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI})
    5.25 -    THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
    5.26 +    THEN' resolve_tac ctxt [@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]])
    5.27  
    5.28  
    5.29  fun expand thm ct =
    5.30 @@ -142,7 +142,7 @@
    5.31  fun prove_injectivity ctxt =
    5.32    Old_Z3_Proof_Tools.by_tac ctxt (
    5.33      CONVERSION (Old_SMT_Utils.prop_conv (norm_conv ctxt))
    5.34 -    THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
    5.35 +    THEN' CSUBGOAL (uncurry (resolve_tac ctxt o single o prove_inj_eq ctxt)))
    5.36  
    5.37  end
    5.38  
     6.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sat Jul 18 20:37:16 2015 +0200
     6.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sat Jul 18 20:47:08 2015 +0200
     6.3 @@ -413,7 +413,7 @@
     6.4      @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
     6.5  
     6.6    fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = (
     6.7 -    rtac thm ORELSE'
     6.8 +    resolve_tac ctxt [thm] ORELSE'
     6.9      (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE'
    6.10      (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st
    6.11  
    6.12 @@ -602,7 +602,7 @@
    6.13  in
    6.14  fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
    6.15    REPEAT_ALL_NEW (match_tac ctxt [rule])
    6.16 -  THEN' rtac @{thm excluded_middle})
    6.17 +  THEN' resolve_tac ctxt @{thms excluded_middle})
    6.18  end
    6.19  
    6.20  
    6.21 @@ -640,10 +640,10 @@
    6.22    apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
    6.23  
    6.24  fun discharge_sk_tac ctxt i st = (
    6.25 -  rtac @{thm trans} i
    6.26 +  resolve_tac ctxt @{thms trans} i
    6.27    THEN resolve_tac ctxt sk_rules i
    6.28 -  THEN (rtac @{thm refl} ORELSE' discharge_sk_tac ctxt) (i+1)
    6.29 -  THEN rtac @{thm refl} i) st
    6.30 +  THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1)
    6.31 +  THEN resolve_tac ctxt @{thms refl} i) st
    6.32  
    6.33  end
    6.34  
    6.35 @@ -715,14 +715,14 @@
    6.36          THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
    6.37      Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
    6.38        Old_Z3_Proof_Tools.by_tac ctxt' (
    6.39 -        (rtac @{thm iff_allI} ORELSE' K all_tac)
    6.40 +        (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
    6.41          THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
    6.42          THEN_ALL_NEW (
    6.43            NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
    6.44            ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
    6.45      Old_Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
    6.46        Old_Z3_Proof_Tools.by_tac ctxt' (
    6.47 -        (rtac @{thm iff_allI} ORELSE' K all_tac)
    6.48 +        (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
    6.49          THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
    6.50          THEN_ALL_NEW (
    6.51            NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
    6.52 @@ -731,7 +731,7 @@
    6.53      Old_Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
    6.54        (fn ctxt' =>
    6.55          Old_Z3_Proof_Tools.by_tac ctxt' (
    6.56 -          (rtac @{thm iff_allI} ORELSE' K all_tac)
    6.57 +          (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
    6.58            THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
    6.59            THEN_ALL_NEW (
    6.60              NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
     7.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Jul 18 20:37:16 2015 +0200
     7.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Jul 18 20:47:08 2015 +0200
     7.3 @@ -1007,12 +1007,12 @@
     7.4        else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
     7.5    in () end
     7.6  
     7.7 -fun core_sos_tac print_cert prover = SUBPROOF (fn {concl, context, ...} =>
     7.8 +fun core_sos_tac print_cert prover = SUBPROOF (fn {concl, context = ctxt, ...} =>
     7.9    let
    7.10      val _ = check_sos known_sos_constants concl
    7.11 -    val (ths, certificates) = real_sos prover context (Thm.dest_arg concl)
    7.12 +    val (th, certificates) = real_sos prover ctxt (Thm.dest_arg concl)
    7.13      val _ = print_cert certificates
    7.14 -  in rtac ths 1 end);
    7.15 +  in resolve_tac ctxt [th] 1 end);
    7.16  
    7.17  fun default_SOME _ NONE v = SOME v
    7.18    | default_SOME _ (SOME v) _ = SOME v;
    7.19 @@ -1050,7 +1050,7 @@
    7.20            instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
    7.21              (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
    7.22               else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
    7.23 -      in rtac th i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
    7.24 +      in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
    7.25  
    7.26  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
    7.27  
     8.1 --- a/src/HOL/Library/bnf_lfp_countable.ML	Sat Jul 18 20:37:16 2015 +0200
     8.2 +++ b/src/HOL/Library/bnf_lfp_countable.ML	Sat Jul 18 20:47:08 2015 +0200
     8.3 @@ -29,11 +29,13 @@
     8.4  
     8.5  fun meta_spec_mp_tac ctxt 0 = K all_tac
     8.6    | meta_spec_mp_tac ctxt depth =
     8.7 -    dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN' dtac ctxt meta_mp THEN' atac;
     8.8 +    dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN'
     8.9 +    dtac ctxt meta_mp THEN' assume_tac ctxt;
    8.10  
    8.11  fun use_induction_hypothesis_tac ctxt =
    8.12    DEEPEN (1, 64 (* large number *))
    8.13 -    (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN' atac THEN' atac) 0;
    8.14 +    (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN'
    8.15 +      assume_tac ctxt THEN' assume_tac ctxt) 0;
    8.16  
    8.17  val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
    8.18    id_apply snd_conv simp_thms};
    8.19 @@ -44,7 +46,7 @@
    8.20        (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
    8.21      TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW
    8.22      REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW
    8.23 -    (atac ORELSE' use_induction_hypothesis_tac ctxt));
    8.24 +    (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt));
    8.25  
    8.26  fun distinct_ctrs_tac ctxt recs =
    8.27    HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
     9.1 --- a/src/HOL/Library/old_recdef.ML	Sat Jul 18 20:37:16 2015 +0200
     9.2 +++ b/src/HOL/Library/old_recdef.ML	Sat Jul 18 20:47:08 2015 +0200
     9.3 @@ -262,19 +262,20 @@
     9.4  struct
     9.5  
     9.6  (* make a casethm from an induction thm *)
     9.7 -val cases_thm_of_induct_thm =
     9.8 -     Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
     9.9 +fun cases_thm_of_induct_thm ctxt =
    9.10 +  Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i)));
    9.11  
    9.12  (* get the case_thm (my version) from a type *)
    9.13 -fun case_thm_of_ty thy ty  =
    9.14 +fun case_thm_of_ty ctxt ty  =
    9.15      let
    9.16 +      val thy = Proof_Context.theory_of ctxt
    9.17        val ty_str = case ty of
    9.18                       Type(ty_str, _) => ty_str
    9.19                     | TFree(s,_)  => error ("Free type: " ^ s)
    9.20                     | TVar((s,_),_) => error ("Free variable: " ^ s)
    9.21        val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
    9.22      in
    9.23 -      cases_thm_of_induct_thm induct
    9.24 +      cases_thm_of_induct_thm ctxt induct
    9.25      end;
    9.26  
    9.27  
    9.28 @@ -287,7 +288,7 @@
    9.29        val x = Free(vstr,ty);
    9.30        val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
    9.31  
    9.32 -      val case_thm = case_thm_of_ty thy ty;
    9.33 +      val case_thm = case_thm_of_ty ctxt ty;
    9.34  
    9.35        val abs_ct = Thm.cterm_of ctxt abst;
    9.36        val free_ct = Thm.cterm_of ctxt x;
    9.37 @@ -2640,7 +2641,8 @@
    9.38  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
    9.39  fun meta_outer ctxt =
    9.40    curry_rule ctxt o Drule.export_without_context o
    9.41 -  rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' etac conjE)));
    9.42 +  rule_by_tactic ctxt
    9.43 +    (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' eresolve_tac ctxt [conjE])));
    9.44  
    9.45  (*Strip off the outer !P*)
    9.46  val spec'=
    10.1 --- a/src/HOL/List.thy	Sat Jul 18 20:37:16 2015 +0200
    10.2 +++ b/src/HOL/List.thy	Sat Jul 18 20:47:08 2015 +0200
    10.3 @@ -621,23 +621,25 @@
    10.4      | NONE => NONE)
    10.5    end
    10.6  
    10.7 -fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
    10.8 +fun tac ctxt [] =
    10.9 +      resolve_tac ctxt [set_singleton] 1 ORELSE
   10.10 +      resolve_tac ctxt [inst_Collect_mem_eq] 1
   10.11    | tac ctxt (If :: cont) =
   10.12        Splitter.split_tac ctxt @{thms split_if} 1
   10.13 -      THEN rtac @{thm conjI} 1
   10.14 -      THEN rtac @{thm impI} 1
   10.15 +      THEN resolve_tac ctxt @{thms conjI} 1
   10.16 +      THEN resolve_tac ctxt @{thms impI} 1
   10.17        THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
   10.18          CONVERSION (right_hand_set_comprehension_conv (K
   10.19            (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
   10.20             then_conv
   10.21             rewr_conv' @{lemma "(True \<and> P) = P" by simp})) ctxt') 1) ctxt 1
   10.22        THEN tac ctxt cont
   10.23 -      THEN rtac @{thm impI} 1
   10.24 +      THEN resolve_tac ctxt @{thms impI} 1
   10.25        THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
   10.26            CONVERSION (right_hand_set_comprehension_conv (K
   10.27              (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
   10.28               then_conv rewr_conv' @{lemma "(False \<and> P) = False" by simp})) ctxt') 1) ctxt 1
   10.29 -      THEN rtac set_Nil_I 1
   10.30 +      THEN resolve_tac ctxt [set_Nil_I] 1
   10.31    | tac ctxt (Case (T, i) :: cont) =
   10.32        let
   10.33          val SOME {injects, distincts, case_thms, split, ...} =
   10.34 @@ -646,9 +648,9 @@
   10.35          (* do case distinction *)
   10.36          Splitter.split_tac ctxt [split] 1
   10.37          THEN EVERY (map_index (fn (i', _) =>
   10.38 -          (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
   10.39 -          THEN REPEAT_DETERM (rtac @{thm allI} 1)
   10.40 -          THEN rtac @{thm impI} 1
   10.41 +          (if i' < length case_thms - 1 then resolve_tac ctxt @{thms conjI} 1 else all_tac)
   10.42 +          THEN REPEAT_DETERM (resolve_tac ctxt @{thms allI} 1)
   10.43 +          THEN resolve_tac ctxt @{thms impI} 1
   10.44            THEN (if i' = i then
   10.45              (* continue recursively *)
   10.46              Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
   10.47 @@ -683,7 +685,7 @@
   10.48                          Conv.repeat_conv
   10.49                            (Conv.bottom_conv
   10.50                              (K (rewr_conv' @{lemma "(\<exists>x. P) = P" by simp})) ctxt'')) ctxt'))) 1) ctxt 1
   10.51 -            THEN rtac set_Nil_I 1)) case_thms)
   10.52 +            THEN resolve_tac ctxt [set_Nil_I] 1)) case_thms)
   10.53        end
   10.54  
   10.55  in
    11.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 20:37:16 2015 +0200
    11.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 20:47:08 2015 +0200
    11.3 @@ -456,7 +456,7 @@
    11.4      val wits = map (fn t => fold absfree (Term.add_frees t []) t)
    11.5        (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
    11.6  
    11.7 -    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    11.8 +    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
    11.9  
   11.10      val (bnf', lthy') =
   11.11        bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs))
   11.12 @@ -547,7 +547,7 @@
   11.13  
   11.14      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   11.15  
   11.16 -    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   11.17 +    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
   11.18  
   11.19      val (bnf', lthy') =
   11.20        bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
   11.21 @@ -629,7 +629,7 @@
   11.22  
   11.23      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   11.24  
   11.25 -    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   11.26 +    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
   11.27  
   11.28      val (bnf', lthy') =
   11.29        bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
   11.30 @@ -883,8 +883,9 @@
   11.31            (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
   11.32        (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   11.33  
   11.34 -    fun wit_tac ctxt = ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN
   11.35 -      mk_simple_wit_tac (wit_thms_of_bnf bnf);
   11.36 +    fun wit_tac ctxt =
   11.37 +      ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN
   11.38 +      mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
   11.39  
   11.40      val (bnf', lthy') =
   11.41        bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
    12.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    12.3 @@ -30,7 +30,7 @@
    12.4  
    12.5    val mk_le_rel_OO_tac: Proof.context -> thm -> thm -> thm list -> tactic
    12.6    val mk_simple_rel_OO_Grp_tac: Proof.context -> thm -> thm -> tactic
    12.7 -  val mk_simple_wit_tac: thm list -> tactic
    12.8 +  val mk_simple_wit_tac: Proof.context -> thm list -> tactic
    12.9    val mk_simplified_set_tac: Proof.context -> thm -> tactic
   12.10    val bd_ordIso_natLeq_tac: tactic
   12.11  end;
   12.12 @@ -98,7 +98,7 @@
   12.13              rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union),
   12.14              rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I}, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2},
   12.15              rtac ctxt @{thm insertI1}, rtac ctxt (o_apply RS equalityD2 RS set_mp),
   12.16 -            etac ctxt @{thm imageI}, atac])
   12.17 +            etac ctxt @{thm imageI}, assume_tac ctxt])
   12.18            comp_set_alts))
   12.19        map_cong0s) 1)
   12.20    end;
   12.21 @@ -158,8 +158,8 @@
   12.22      unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
   12.23      (REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
   12.24       REPEAT_DETERM (CHANGED ((
   12.25 -       (rtac ctxt conjI THEN' (atac ORELSE' rtac ctxt subset_UNIV)) ORELSE'
   12.26 -       atac ORELSE'
   12.27 +       (rtac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt subset_UNIV)) ORELSE'
   12.28 +       assume_tac ctxt ORELSE'
   12.29         (rtac ctxt subset_UNIV)) 1)) ORELSE rtac ctxt subset_UNIV 1));
   12.30  
   12.31  val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def UN_insert UN_empty Un_empty_right
   12.32 @@ -170,13 +170,13 @@
   12.33    ALLGOALS (dtac ctxt @{thm in_Union_o_assoc}) THEN
   12.34    unfold_thms_tac ctxt [collect_set_map] THEN
   12.35    unfold_thms_tac ctxt comp_wit_thms THEN
   12.36 -  REPEAT_DETERM ((atac ORELSE'
   12.37 +  REPEAT_DETERM ((assume_tac ctxt ORELSE'
   12.38      REPEAT_DETERM o eresolve_tac ctxt @{thms UnionE UnE} THEN'
   12.39      etac ctxt imageE THEN' TRY o dresolve_tac ctxt Gwit_thms THEN'
   12.40      (etac ctxt FalseE ORELSE'
   12.41      hyp_subst_tac ctxt THEN'
   12.42      dresolve_tac ctxt Fwit_thms THEN'
   12.43 -    (etac ctxt FalseE ORELSE' atac))) 1);
   12.44 +    (etac ctxt FalseE ORELSE' assume_tac ctxt))) 1);
   12.45  
   12.46  
   12.47  (* Kill operation *)
   12.48 @@ -190,9 +190,9 @@
   12.49    REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
   12.50    REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
   12.51      rtac ctxt conjI THEN' rtac ctxt subset_UNIV) 1)) THEN
   12.52 -  (rtac ctxt subset_UNIV ORELSE' atac) 1 THEN
   12.53 +  (rtac ctxt subset_UNIV ORELSE' assume_tac ctxt) 1 THEN
   12.54    REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
   12.55 -  REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' atac) 1))) ORELSE
   12.56 +  REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1))) ORELSE
   12.57    ((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
   12.58      REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt subset_UNIV 1));
   12.59  
   12.60 @@ -207,11 +207,11 @@
   12.61  fun lift_in_alt_tac ctxt =
   12.62    ((rtac ctxt @{thm Collect_cong} THEN' rtac ctxt iffI) 1 THEN
   12.63    REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
   12.64 -  REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' atac) 1)) THEN
   12.65 +  REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1)) THEN
   12.66    REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
   12.67    REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
   12.68      rtac ctxt conjI THEN' rtac ctxt @{thm empty_subsetI}) 1)) THEN
   12.69 -  (rtac ctxt @{thm empty_subsetI} ORELSE' atac) 1) ORELSE
   12.70 +  (rtac ctxt @{thm empty_subsetI} ORELSE' assume_tac ctxt) 1) ORELSE
   12.71    ((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
   12.72      REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt @{thm empty_subsetI} 1));
   12.73  
   12.74 @@ -232,7 +232,8 @@
   12.75  fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm =
   12.76    rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
   12.77  
   12.78 -fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve0_tac (@{thm emptyE} :: wit_thms));
   12.79 +fun mk_simple_wit_tac ctxt wit_thms =
   12.80 +  ALLGOALS (assume_tac ctxt ORELSE' eresolve0_tac (@{thm emptyE} :: wit_thms));
   12.81  
   12.82  val csum_thms =
   12.83    @{thms csum_cong1 csum_cong2 csum_cong  csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
    13.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    13.3 @@ -53,15 +53,15 @@
    13.4  fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
    13.5  fun mk_map_cong_tac ctxt cong0 =
    13.6    (hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'
    13.7 -   REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' atac)) 1;
    13.8 +   REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1;
    13.9  fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest};
   13.10  fun mk_in_mono_tac ctxt n = if n = 0 then rtac ctxt subset_UNIV 1
   13.11    else (rtac ctxt subsetI THEN'
   13.12    rtac ctxt CollectI) 1 THEN
   13.13    REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN
   13.14    REPEAT_DETERM_N (n - 1)
   13.15 -    ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' atac) 1) THEN
   13.16 -  (etac ctxt subset_trans THEN' atac) 1;
   13.17 +    ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
   13.18 +  (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
   13.19  
   13.20  fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
   13.21    let
   13.22 @@ -70,7 +70,7 @@
   13.23    in
   13.24      HEADGOAL (rtac ctxt @{thm injI} THEN' etac ctxt (map_cong' RS box_equals) THEN'
   13.25        REPEAT_DETERM_N 2 o (rtac ctxt (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN'
   13.26 -        REPEAT_DETERM_N n o atac))
   13.27 +        REPEAT_DETERM_N n o assume_tac ctxt))
   13.28    end;
   13.29  
   13.30  fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
   13.31 @@ -104,10 +104,12 @@
   13.32          REPEAT_DETERM o
   13.33            eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
   13.34          hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
   13.35 -        REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_split_Grp_eqD}, etac ctxt @{thm set_mp}, atac],
   13.36 +        REPEAT_DETERM_N n o
   13.37 +          EVERY' [rtac ctxt @{thm Collect_split_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
   13.38          rtac ctxt CollectI,
   13.39          CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
   13.40 -          rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_split_Grp_inD}, etac ctxt @{thm set_mp}, atac])
   13.41 +          rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_split_Grp_inD},
   13.42 +          etac ctxt @{thm set_mp}, assume_tac ctxt])
   13.43          set_maps,
   13.44          rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE],
   13.45          hyp_subst_tac ctxt,
   13.46 @@ -120,7 +122,7 @@
   13.47              rtac ctxt CollectI,
   13.48              CONJ_WRAP' (fn thm =>
   13.49                EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
   13.50 -                rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, atac])
   13.51 +                rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt])
   13.52              set_maps])
   13.53            @{thms fst_convol snd_convol} [map_id, refl])] 1
   13.54    end;
   13.55 @@ -146,11 +148,11 @@
   13.56        unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
   13.57        TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
   13.58          resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
   13.59 -        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, atac,
   13.60 +        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, assume_tac ctxt,
   13.61          rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
   13.62          CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
   13.63          REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
   13.64 -        dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, atac])
   13.65 +        dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
   13.66      end;
   13.67  
   13.68  fun mk_rel_mono_tac ctxt rel_OO_Grps in_mono =
   13.69 @@ -194,7 +196,7 @@
   13.70      val n = length set_maps;
   13.71      fun in_tac nthO_in = rtac ctxt CollectI THEN'
   13.72          CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
   13.73 -          rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, atac]) set_maps;
   13.74 +          rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps;
   13.75      val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
   13.76        else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
   13.77          rtac ctxt (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
   13.78 @@ -213,8 +215,8 @@
   13.79          rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
   13.80          REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply,
   13.81            rtac ctxt ballE, rtac ctxt subst,
   13.82 -          rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, atac, etac ctxt notE,
   13.83 -          etac ctxt set_mp, atac],
   13.84 +          rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt,
   13.85 +          etac ctxt notE, etac ctxt set_mp, assume_tac ctxt],
   13.86          in_tac @{thm fstOp_in},
   13.87          rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
   13.88          rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
   13.89 @@ -226,14 +228,14 @@
   13.90    end;
   13.91  
   13.92  fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
   13.93 -  if null set_maps then atac 1
   13.94 +  if null set_maps then assume_tac ctxt 1
   13.95    else
   13.96      unfold_tac ctxt [in_rel] THEN
   13.97      REPEAT_DETERM (eresolve_tac ctxt [exE, CollectE, conjE] 1) THEN
   13.98      hyp_subst_tac ctxt 1 THEN
   13.99      EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]},
  13.100        CONJ_WRAP' (fn thm =>
  13.101 -        (etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac))
  13.102 +        (etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' assume_tac ctxt))
  13.103        set_maps] 1;
  13.104  
  13.105  fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong =
  13.106 @@ -241,7 +243,7 @@
  13.107      fun last_tac iffD =
  13.108        HEADGOAL (etac ctxt rel_mono_strong) THEN
  13.109        REPEAT_DETERM (HEADGOAL (etac ctxt (@{thm predicate2_transferD} RS iffD) THEN'
  13.110 -        REPEAT_DETERM o atac));
  13.111 +        REPEAT_DETERM o assume_tac ctxt));
  13.112    in
  13.113      REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
  13.114      (HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
  13.115 @@ -262,7 +264,8 @@
  13.116    in
  13.117      REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN
  13.118      unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
  13.119 -    HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono, REPEAT_DETERM_N n o atac,
  13.120 +    HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono,
  13.121 +      REPEAT_DETERM_N n o assume_tac ctxt,
  13.122        rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1),
  13.123        REPEAT_DETERM o eresolve_tac ctxt [exE, CollectE, conjE], hyp_subst_tac ctxt,
  13.124        rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac,
  13.125 @@ -316,12 +319,12 @@
  13.126          else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
  13.127          rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I},
  13.128          CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI})
  13.129 -          (K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' atac)) set_maps,
  13.130 +          (K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' assume_tac ctxt)) set_maps,
  13.131          rtac ctxt sym,
  13.132          rtac ctxt (Drule.rotate_prems 1
  13.133             ((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
  13.134               map_comp RS sym, map_id]) RSN (2, trans))),
  13.135 -        REPEAT_DETERM_N (2 * live) o atac,
  13.136 +        REPEAT_DETERM_N (2 * live) o assume_tac ctxt,
  13.137          REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans),
  13.138          rtac ctxt refl,
  13.139          rtac ctxt @{thm surj_imp_ordLeq}, rtac ctxt subsetI, rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
  13.140 @@ -335,8 +338,10 @@
  13.141    end;
  13.142  
  13.143  fun mk_trivial_wit_tac ctxt wit_defs set_maps =
  13.144 -  unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm =>
  13.145 -    dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' atac) set_maps)) THEN ALLGOALS atac;
  13.146 +  unfold_thms_tac ctxt wit_defs THEN
  13.147 +  HEADGOAL (EVERY' (map (fn thm =>
  13.148 +    dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' assume_tac ctxt) set_maps)) THEN
  13.149 +  ALLGOALS (assume_tac ctxt);
  13.150  
  13.151  fun mk_set_transfer_tac ctxt in_rel set_maps =
  13.152    Goal.conjunction_tac 1 THEN
  13.153 @@ -345,7 +350,7 @@
  13.154      @{thms exE conjE CollectE}))) THEN
  13.155    HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
  13.156      rtac ctxt @{thm rel_setI}) THEN
  13.157 -  REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' atac THEN'
  13.158 +  REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
  13.159      REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
  13.160      rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps);
  13.161  
    14.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    14.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    14.3 @@ -113,39 +113,40 @@
    14.4      unfold_thms_tac ctxt cases THEN
    14.5      ALLGOALS (fn k => (select_prem_tac ctxt n (dtac ctxt asm_rl) k) k) THEN
    14.6      ALLGOALS (REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt rel_funD THEN'
    14.7 -      (atac THEN' etac ctxt thin_rl ORELSE' rtac ctxt refl)) THEN' atac)
    14.8 +      (assume_tac ctxt THEN' etac ctxt thin_rl ORELSE' rtac ctxt refl)) THEN' assume_tac ctxt)
    14.9    end;
   14.10  
   14.11  fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
   14.12    HEADGOAL Goal.conjunction_tac THEN
   14.13    ALLGOALS (REPEAT o (resolve_tac ctxt (rel_funI :: rel_intros) THEN'
   14.14 -    TRY o (REPEAT_DETERM1 o (atac ORELSE'
   14.15 +    TRY o (REPEAT_DETERM1 o (assume_tac ctxt ORELSE'
   14.16        K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac ctxt refl))));
   14.17  
   14.18  fun mk_disc_transfer_tac ctxt rel_sel exhaust_disc distinct_disc =
   14.19    let
   14.20      fun last_disc_tac iffD =
   14.21 -      HEADGOAL (rtac ctxt (rotate_prems ~1 exhaust_disc) THEN' atac THEN'
   14.22 -      REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt (rotate_prems 1 iffD) THEN' atac THEN'
   14.23 -        rotate_tac ~1 THEN' etac ctxt (rotate_prems 1 notE) THEN' eresolve0_tac distinct_disc));
   14.24 +      HEADGOAL (rtac ctxt (rotate_prems ~1 exhaust_disc) THEN' assume_tac ctxt THEN'
   14.25 +      REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt (rotate_prems 1 iffD) THEN'
   14.26 +        assume_tac ctxt THEN' rotate_tac ~1 THEN'
   14.27 +        etac ctxt (rotate_prems 1 notE) THEN' eresolve0_tac distinct_disc));
   14.28    in
   14.29      HEADGOAL Goal.conjunction_tac THEN
   14.30      REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI THEN' dtac ctxt (rel_sel RS iffD1) THEN'
   14.31 -      REPEAT_DETERM o (etac ctxt conjE) THEN' (atac ORELSE' rtac ctxt iffI))) THEN
   14.32 +      REPEAT_DETERM o (etac ctxt conjE) THEN' (assume_tac ctxt ORELSE' rtac ctxt iffI))) THEN
   14.33      TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)
   14.34    end;
   14.35  
   14.36  fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
   14.37    unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac ctxt sumEN') THEN
   14.38    HEADGOAL (EVERY' (maps (fn k => [select_prem_tac ctxt n (rotate_tac 1) k,
   14.39 -    REPEAT_DETERM o dtac ctxt meta_spec, etac ctxt meta_mp, atac]) (1 upto n)));
   14.40 +    REPEAT_DETERM o dtac ctxt meta_spec, etac ctxt meta_mp, assume_tac ctxt]) (1 upto n)));
   14.41  
   14.42  fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor =
   14.43    HEADGOAL (rtac ctxt iffI THEN'
   14.44      EVERY' (@{map 3} (fn cTs => fn cx => fn th =>
   14.45        dtac ctxt (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
   14.46        SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
   14.47 -      atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
   14.48 +      assume_tac ctxt) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
   14.49  
   14.50  fun mk_half_distinct_tac ctxt ctor_inject abs_inject ctr_defs =
   14.51    unfold_thms_tac ctxt (ctor_inject :: abs_inject :: @{thms sum.inject} @ ctr_defs) THEN
   14.52 @@ -204,7 +205,7 @@
   14.53                     [mk_rel_funDN 2 case_sum_transfer_eq, mk_rel_funDN 2 case_sum_transfer])) THEN
   14.54                   HEADGOAL (select_prem_tac ctxt total_n (dtac ctxt asm_rl) (acc + n)) THEN
   14.55                   HEADGOAL (SELECT_GOAL (HEADGOAL
   14.56 -                   (REPEAT_DETERM o (atac ORELSE' resolve_tac ctxt
   14.57 +                   (REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt
   14.58                         [mk_rel_funDN 1 case_prod_transfer_eq,
   14.59                          mk_rel_funDN 1 case_prod_transfer,
   14.60                          rel_funI]) THEN_ALL_NEW
   14.61 @@ -255,12 +256,12 @@
   14.62        HEADGOAL (Inl_Inr_Pair_tac THEN'
   14.63          rtac ctxt (mk_rel_funDN 3 @{thm If_transfer}) THEN'
   14.64          select_prem_tac ctxt total (dtac ctxt asm_rl) pos THEN'
   14.65 -        dtac ctxt rel_funD THEN' atac THEN' atac);
   14.66 +        dtac ctxt rel_funD THEN' assume_tac ctxt THEN' assume_tac ctxt);
   14.67  
   14.68      fun mk_unfold_Inl_Inr_Pair_tac total pos =
   14.69        HEADGOAL (Inl_Inr_Pair_tac THEN'
   14.70          select_prem_tac ctxt total (dtac ctxt asm_rl) pos THEN'
   14.71 -        dtac ctxt rel_funD THEN' atac THEN' atac);
   14.72 +        dtac ctxt rel_funD THEN' assume_tac ctxt THEN' assume_tac ctxt);
   14.73  
   14.74      fun mk_unfold_arg_tac qs gs =
   14.75        EVERY (map (mk_unfold_If_tac num_pgs o prem_no_of) qs) THEN
   14.76 @@ -307,7 +308,7 @@
   14.77  fun solve_prem_prem_tac ctxt =
   14.78    REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE' rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE'
   14.79      hyp_subst_tac ctxt ORELSE' resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
   14.80 -  (rtac ctxt refl ORELSE' atac ORELSE' rtac ctxt @{thm singletonI});
   14.81 +  (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' rtac ctxt @{thm singletonI});
   14.82  
   14.83  fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
   14.84      pre_set_defs =
   14.85 @@ -323,7 +324,7 @@
   14.86        REPEAT_DETERM_N m o (dtac ctxt meta_spec THEN' rotate_tac ~1)]) THEN
   14.87      EVERY [REPEAT_DETERM_N r
   14.88          (HEADGOAL (rotate_tac ~1 THEN' dtac ctxt meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
   14.89 -      if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
   14.90 +      if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL (assume_tac ctxt),
   14.91        mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
   14.92          pre_set_defs]
   14.93    end;
   14.94 @@ -349,10 +350,10 @@
   14.95    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
   14.96    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
   14.97      sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
   14.98 -  (atac ORELSE' REPEAT o etac ctxt conjE THEN'
   14.99 +  (assume_tac ctxt ORELSE' REPEAT o etac ctxt conjE THEN'
  14.100       full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
  14.101       REPEAT o etac ctxt conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
  14.102 -     REPEAT o (resolve_tac ctxt [refl, conjI] ORELSE' atac));
  14.103 +     REPEAT o (resolve_tac ctxt [refl, conjI] ORELSE' assume_tac ctxt));
  14.104  
  14.105  fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
  14.106    let
  14.107 @@ -367,8 +368,8 @@
  14.108      dtor_ctor exhaust ctr_defs discss selss =
  14.109    let val ks = 1 upto n in
  14.110      EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
  14.111 -        dtac ctxt meta_spec, dtac ctxt meta_mp, atac, rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 0),
  14.112 -        hyp_subst_tac ctxt] @
  14.113 +        dtac ctxt meta_spec, dtac ctxt meta_mp, assume_tac ctxt, rtac ctxt exhaust,
  14.114 +        K (co_induct_inst_as_projs_tac ctxt 0), hyp_subst_tac ctxt] @
  14.115        @{map 4} (fn k => fn ctr_def => fn discs => fn sels =>
  14.116          EVERY' ([rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
  14.117            map2 (fn k' => fn discs' =>
  14.118 @@ -413,7 +414,7 @@
  14.119      True_implies_equals conj_imp_eq_imp_imp} @
  14.120      map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
  14.121      map (fn thm => thm RS eqTrueI) rel_injects) THEN
  14.122 -  TRYALL (atac ORELSE' etac ctxt FalseE ORELSE'
  14.123 +  TRYALL (assume_tac ctxt ORELSE' etac ctxt FalseE ORELSE'
  14.124      (REPEAT_DETERM o dtac ctxt @{thm meta_spec} THEN'
  14.125       TRY o filter_prems_tac ctxt
  14.126         (forall (curry (op <>) (HOLogic.mk_Trueprop @{term False})) o Logic.strip_imp_prems) THEN'
  14.127 @@ -427,7 +428,7 @@
  14.128        (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
  14.129           (dtac ctxt (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct]
  14.130              @{thm arg_cong2} RS iffD1)) THEN'
  14.131 -          atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac ctxt assm THEN'
  14.132 +          assume_tac ctxt THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt THEN' dtac ctxt assm THEN'
  14.133            REPEAT_DETERM o etac ctxt conjE))) 1 THEN
  14.134        unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
  14.135        unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
  14.136 @@ -435,7 +436,7 @@
  14.137          @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False
  14.138            iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
  14.139        REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN' (REPEAT_DETERM o rtac ctxt conjI) THEN'
  14.140 -        (rtac ctxt refl ORELSE' atac))))
  14.141 +        (rtac ctxt refl ORELSE' assume_tac ctxt))))
  14.142      cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
  14.143        abs_inverses);
  14.144  
  14.145 @@ -445,13 +446,14 @@
  14.146        fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
  14.147          HEADGOAL (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
  14.148            (rtac ctxt (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
  14.149 -            THEN' atac THEN' atac THEN' TRY o resolve_tac ctxt assms))) THEN
  14.150 +            THEN' assume_tac ctxt THEN' assume_tac ctxt THEN' TRY o resolve_tac ctxt assms))) THEN
  14.151          unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
  14.152            @{thms id_bnf_def vimage2p_def}) THEN
  14.153          TRYALL (hyp_subst_tac ctxt) THEN
  14.154          unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
  14.155            Inr_Inl_False  sum.inject prod.inject}) THEN
  14.156 -        TRYALL (rtac ctxt refl ORELSE' etac ctxt FalseE ORELSE' (REPEAT_DETERM o etac ctxt conjE) THEN' atac))
  14.157 +        TRYALL (rtac ctxt refl ORELSE' etac ctxt FalseE ORELSE'
  14.158 +          (REPEAT_DETERM o etac ctxt conjE) THEN' assume_tac ctxt))
  14.159      cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
  14.160  
  14.161  fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts rel_eqs =
  14.162 @@ -467,7 +469,7 @@
  14.163    TRYALL Goal.conjunction_tac THEN
  14.164    unfold_thms_tac ctxt (map (Drule.abs_def o Local_Defs.meta_rewrite_rule ctxt) sel_defs) THEN
  14.165    ALLGOALS (rtac ctxt (mk_rel_funDN n case_transfer) THEN_ALL_NEW
  14.166 -    REPEAT_DETERM o (atac ORELSE' rtac ctxt rel_funI));
  14.167 +    REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt rel_funI));
  14.168  
  14.169  fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
  14.170    TRYALL Goal.conjunction_tac THEN
  14.171 @@ -480,7 +482,7 @@
  14.172      ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE'
  14.173          eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE'
  14.174          hyp_subst_tac ctxt) THEN'
  14.175 -      (rtac ctxt @{thm singletonI} ORELSE' atac));
  14.176 +      (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
  14.177  
  14.178  fun mk_set_cases_tac ctxt ct assms exhaust sets =
  14.179    HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
  14.180 @@ -488,13 +490,14 @@
  14.181    REPEAT_DETERM (HEADGOAL
  14.182      (eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
  14.183       hyp_subst_tac ctxt ORELSE'
  14.184 -     SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o atac)))));
  14.185 +     SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o assume_tac ctxt)))));
  14.186  
  14.187  fun mk_set_intros_tac ctxt sets =
  14.188    TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN
  14.189    TRYALL (REPEAT o
  14.190      (resolve_tac ctxt @{thms UnI1 UnI2} ORELSE'
  14.191 -     eresolve_tac ctxt @{thms UN_I UN_I[rotated]}) THEN' (rtac ctxt @{thm singletonI} ORELSE' atac));
  14.192 +     eresolve_tac ctxt @{thms UN_I UN_I[rotated]}) THEN'
  14.193 +     (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
  14.194  
  14.195  fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
  14.196      Abs_pre_inverses =
  14.197 @@ -502,7 +505,7 @@
  14.198      val assms_tac =
  14.199        let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in
  14.200          fold (curry (op ORELSE')) (map (fn thm =>
  14.201 -            funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' atac) (rtac ctxt thm)) assms')
  14.202 +            funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt) (rtac ctxt thm)) assms')
  14.203            (etac ctxt FalseE)
  14.204        end;
  14.205      val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
  14.206 @@ -512,7 +515,7 @@
  14.207      TRYALL (resolve_tac ctxt exhausts' THEN_ALL_NEW
  14.208        (resolve_tac ctxt (map (fn ct => refl RS
  14.209           cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
  14.210 -        THEN' atac THEN' hyp_subst_tac ctxt)) THEN
  14.211 +        THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt)) THEN
  14.212      unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
  14.213        @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
  14.214          Un_empty_right empty_iff singleton_iff}) THEN
    15.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    15.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    15.3 @@ -53,33 +53,34 @@
    15.4  
    15.5  val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
    15.6  
    15.7 -fun distinct_in_prems_tac distincts =
    15.8 -  eresolve0_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
    15.9 +fun distinct_in_prems_tac ctxt distincts =
   15.10 +  eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
   15.11 +  assume_tac ctxt;
   15.12  
   15.13  fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
   15.14    HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
   15.15  
   15.16  fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
   15.17    let val ks = 1 upto n in
   15.18 -    HEADGOAL (atac ORELSE'
   15.19 +    HEADGOAL (assume_tac ctxt ORELSE'
   15.20        cut_tac nchotomy THEN'
   15.21        K (exhaust_inst_as_projs_tac ctxt frees) THEN'
   15.22        EVERY' (map (fn k =>
   15.23            (if k < n then etac ctxt disjE else K all_tac) THEN'
   15.24 -          REPEAT o (dtac ctxt meta_mp THEN' atac ORELSE'
   15.25 -            etac ctxt conjE THEN' dtac ctxt meta_mp THEN' atac ORELSE'
   15.26 -            atac))
   15.27 +          REPEAT o (dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
   15.28 +            etac ctxt conjE THEN' dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
   15.29 +            assume_tac ctxt))
   15.30          ks))
   15.31    end;
   15.32  
   15.33  fun mk_primcorec_assumption_tac ctxt discIs =
   15.34    SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
   15.35        not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
   15.36 -    SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' atac ORELSE' etac ctxt conjE ORELSE'
   15.37 +    SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' etac ctxt conjE ORELSE'
   15.38      eresolve_tac ctxt falseEs ORELSE'
   15.39      resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
   15.40 -    dresolve_tac ctxt discIs THEN' atac ORELSE'
   15.41 -    etac ctxt notE THEN' atac ORELSE'
   15.42 +    dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE'
   15.43 +    etac ctxt notE THEN' assume_tac ctxt ORELSE'
   15.44      etac ctxt disjE))));
   15.45  
   15.46  fun ss_fst_snd_conv ctxt =
   15.47 @@ -120,15 +121,16 @@
   15.48      EVERY' (map (fn [] => etac ctxt FalseE
   15.49          | fun_discs' as [fun_disc'] =>
   15.50            if eq_list Thm.eq_thm (fun_discs', fun_discs) then
   15.51 -            REPEAT_DETERM o etac ctxt conjI THEN' (atac ORELSE' rtac ctxt TrueI)
   15.52 +            REPEAT_DETERM o etac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt TrueI)
   15.53            else
   15.54              rtac ctxt FalseE THEN'
   15.55 -            (rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o atac ORELSE'
   15.56 +            (rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o assume_tac ctxt ORELSE'
   15.57               cut_tac fun_disc') THEN'
   15.58 -            dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' atac)
   15.59 +            dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' assume_tac ctxt)
   15.60        fun_discss) THEN'
   15.61      (etac ctxt FalseE ORELSE'
   15.62 -     resolve_tac ctxt (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
   15.63 +     resolve_tac ctxt
   15.64 +      (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt));
   15.65  
   15.66  fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
   15.67      m excludesss =
   15.68 @@ -139,8 +141,8 @@
   15.69      resolve_tac ctxt split_connectI ORELSE'
   15.70      Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
   15.71      Splitter.split_tac ctxt (split_if :: splits) ORELSE'
   15.72 -    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
   15.73 -    etac ctxt notE THEN' atac ORELSE'
   15.74 +    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' assume_tac ctxt ORELSE'
   15.75 +    etac ctxt notE THEN' assume_tac ctxt ORELSE'
   15.76      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
   15.77           sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
   15.78         mapsx @ map_ident0s @ map_comps))) ORELSE'
   15.79 @@ -150,7 +152,7 @@
   15.80  
   15.81  fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
   15.82    HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
   15.83 -    (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
   15.84 +    (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o assume_tac ctxt) THEN
   15.85    unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl);
   15.86  
   15.87  fun inst_split_eq ctxt split =
   15.88 @@ -174,13 +176,13 @@
   15.89      prelude_tac ctxt [] (fun_ctr RS trans) THEN
   15.90      HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
   15.91        SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
   15.92 -      (rtac ctxt refl ORELSE' atac ORELSE'
   15.93 +      (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
   15.94         resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
   15.95         Splitter.split_tac ctxt (split_if :: splits) ORELSE'
   15.96         Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
   15.97         mk_primcorec_assumption_tac ctxt discIs ORELSE'
   15.98 -       distinct_in_prems_tac distincts ORELSE'
   15.99 -       (TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' atac)))))
  15.100 +       distinct_in_prems_tac ctxt distincts ORELSE'
  15.101 +       (TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' assume_tac ctxt)))))
  15.102    end;
  15.103  
  15.104  fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
  15.105 @@ -207,11 +209,11 @@
  15.106  fun mk_primcorec_code_tac ctxt distincts splits raw =
  15.107    HEADGOAL (rtac ctxt raw ORELSE' rtac ctxt (raw RS trans) THEN'
  15.108      SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
  15.109 -    (rtac ctxt refl ORELSE' atac ORELSE'
  15.110 +    (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
  15.111       resolve_tac ctxt split_connectI ORELSE'
  15.112       Splitter.split_tac ctxt (split_if :: splits) ORELSE'
  15.113 -     distinct_in_prems_tac distincts ORELSE'
  15.114 -     rtac ctxt sym THEN' atac ORELSE'
  15.115 -     etac ctxt notE THEN' atac));
  15.116 +     distinct_in_prems_tac ctxt distincts ORELSE'
  15.117 +     rtac ctxt sym THEN' assume_tac ctxt ORELSE'
  15.118 +     etac ctxt notE THEN' assume_tac ctxt));
  15.119  
  15.120  end;
    16.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    16.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    16.3 @@ -116,15 +116,15 @@
    16.4  fun mk_coalg_set_tac ctxt coalg_def =
    16.5    dtac ctxt (coalg_def RS iffD1) 1 THEN
    16.6    REPEAT_DETERM (etac ctxt conjE 1) THEN
    16.7 -  EVERY' [dtac ctxt rev_bspec, atac] 1 THEN
    16.8 -  REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN atac 1;
    16.9 +  EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
   16.10 +  REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN assume_tac ctxt 1;
   16.11  
   16.12  fun mk_mor_elim_tac ctxt mor_def =
   16.13    (dtac ctxt (mor_def RS iffD1) THEN'
   16.14    REPEAT o etac ctxt conjE THEN'
   16.15    TRY o rtac ctxt @{thm image_subsetI} THEN'
   16.16    etac ctxt bspec THEN'
   16.17 -  atac) 1;
   16.18 +  assume_tac ctxt) 1;
   16.19  
   16.20  fun mk_mor_incl_tac ctxt mor_def map_ids =
   16.21    (rtac ctxt (mor_def RS iffD2) THEN'
   16.22 @@ -137,10 +137,11 @@
   16.23  fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids =
   16.24    let
   16.25      fun fbetw_tac image = EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
   16.26 -      etac ctxt image, atac];
   16.27 +      etac ctxt image, assume_tac ctxt];
   16.28      fun mor_tac ((mor_image, morE), map_comp_id) =
   16.29        EVERY' [rtac ctxt ballI, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
   16.30 -        etac ctxt (morE RS arg_cong), atac, etac ctxt morE, etac ctxt mor_image, atac];
   16.31 +        etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE,
   16.32 +        etac ctxt mor_image, assume_tac ctxt];
   16.33    in
   16.34      (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
   16.35      CONJ_WRAP' fbetw_tac mor_images THEN'
   16.36 @@ -171,7 +172,7 @@
   16.37  
   16.38  fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i =
   16.39    EVERY' (map (rtac ctxt) [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2,
   16.40 -    rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, atac]) 1;
   16.41 +    rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
   16.42  
   16.43  fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
   16.44    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   16.45 @@ -185,13 +186,13 @@
   16.46          else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
   16.47          CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
   16.48            (K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE],
   16.49 -            rtac ctxt subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
   16.50 +            rtac ctxt subset_trans, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
   16.51        rec_Sucs] 1;
   16.52  
   16.53  fun mk_Jset_minimal_tac ctxt n col_minimal =
   16.54    (CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm UN_least}, rtac ctxt rev_mp, rtac ctxt col_minimal,
   16.55      EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac ctxt impI,
   16.56 -    REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], atac])) (1 upto n)) 1
   16.57 +    REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1
   16.58  
   16.59  fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
   16.60    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   16.61 @@ -204,14 +205,16 @@
   16.62            if m = 0 then K all_tac
   16.63            else EVERY' [rtac ctxt Un_cong, rtac ctxt @{thm box_equals},
   16.64              rtac ctxt (nth passive_set_map0s (j - 1) RS sym),
   16.65 -            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong), atac],
   16.66 +            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong),
   16.67 +            assume_tac ctxt],
   16.68            CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong))
   16.69              (fn (i, (set_map0, coalg_set)) =>
   16.70                EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})),
   16.71 -                etac ctxt (morE RS sym RS arg_cong RS trans), atac, rtac ctxt set_map0,
   16.72 +                etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0,
   16.73                  rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}),
   16.74 -                ftac ctxt coalg_set, atac, dtac ctxt set_mp, atac, rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
   16.75 -                REPEAT_DETERM o etac ctxt allE, atac, atac])
   16.76 +                ftac ctxt coalg_set, assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
   16.77 +                rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
   16.78 +                REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt])
   16.79              (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
   16.80        (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
   16.81  
   16.82 @@ -222,12 +225,12 @@
   16.83  
   16.84      fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
   16.85        EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
   16.86 -        etac ctxt allE, etac ctxt allE, etac ctxt impE, atac, etac ctxt bexE,
   16.87 +        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE,
   16.88          REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
   16.89          rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
   16.90          CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
   16.91            REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
   16.92 -          atac])
   16.93 +          assume_tac ctxt])
   16.94          @{thms fst_diag_id snd_diag_id},
   16.95          rtac ctxt CollectI,
   16.96          CONJ_WRAP' (fn (i, thm) =>
   16.97 @@ -241,24 +244,24 @@
   16.98  
   16.99      fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
  16.100        EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
  16.101 -        etac ctxt allE, etac ctxt allE, etac ctxt impE, atac,
  16.102 +        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
  16.103          dtac ctxt (in_rel RS @{thm iffD1}),
  16.104          REPEAT_DETERM o eresolve0_tac ([CollectE, conjE, exE] @
  16.105            @{thms CollectE Collect_split_in_rel_leE}),
  16.106          rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
  16.107          REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
  16.108          REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
  16.109 -        atac, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
  16.110 +        assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
  16.111          REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
  16.112          REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
  16.113          rtac ctxt trans, rtac ctxt map_cong0,
  16.114 -        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, atac],
  16.115 +        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, assume_tac ctxt],
  16.116          REPEAT_DETERM_N n o rtac ctxt refl,
  16.117 -        atac, rtac ctxt CollectI,
  16.118 +        assume_tac ctxt, rtac ctxt CollectI,
  16.119          CONJ_WRAP' (fn (i, thm) =>
  16.120            if i <= m then rtac ctxt subset_UNIV
  16.121            else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
  16.122 -            rtac ctxt trans_fun_cong_image_id_id_apply, atac])
  16.123 +            rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt])
  16.124          (1 upto (m + n) ~~ set_map0s)];
  16.125    in
  16.126      EVERY' [rtac ctxt (bis_def RS trans),
  16.127 @@ -283,7 +286,7 @@
  16.128  fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs =
  16.129    EVERY' [rtac ctxt (bis_rel RS iffD2), REPEAT_DETERM o dtac ctxt (bis_rel RS iffD1),
  16.130      REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
  16.131 -    CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, atac])) rel_congs,
  16.132 +    CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, assume_tac ctxt])) rel_congs,
  16.133      CONJ_WRAP' (fn (rel_cong, le_rel_OO) =>
  16.134        EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
  16.135          rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
  16.136 @@ -294,7 +297,7 @@
  16.137          REPEAT_DETERM o dtac ctxt prod_injectD,
  16.138          etac ctxt conjE, hyp_subst_tac ctxt,
  16.139          REPEAT_DETERM o etac ctxt allE, rtac ctxt @{thm relcomppI},
  16.140 -        etac ctxt mp, atac, etac ctxt mp, atac]) (rel_congs ~~ le_rel_OOs)] 1;
  16.141 +        etac ctxt mp, assume_tac ctxt, etac ctxt mp, assume_tac ctxt]) (rel_congs ~~ le_rel_OOs)] 1;
  16.142  
  16.143  fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
  16.144    unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
  16.145 @@ -313,14 +316,15 @@
  16.146      unfold_thms_tac ctxt [bis_def] THEN
  16.147      EVERY' [rtac ctxt conjI,
  16.148        CONJ_WRAP' (fn i =>
  16.149 -        EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, atac,
  16.150 +        EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, assume_tac ctxt,
  16.151            dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks,
  16.152        CONJ_WRAP' (fn (i, in_mono) =>
  16.153 -        EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E}, dtac ctxt bspec, atac,
  16.154 +        EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E},
  16.155 +          dtac ctxt bspec, assume_tac ctxt,
  16.156            dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp,
  16.157 -          atac, etac ctxt bexE, rtac ctxt bexI, atac, rtac ctxt in_mono,
  16.158 +          assume_tac ctxt, etac ctxt bexE, rtac ctxt bexI, assume_tac ctxt, rtac ctxt in_mono,
  16.159            REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]},
  16.160 -          atac]) (ks ~~ in_monos)] 1
  16.161 +          assume_tac ctxt]) (ks ~~ in_monos)] 1
  16.162    end;
  16.163  
  16.164  fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
  16.165 @@ -334,15 +338,15 @@
  16.166  
  16.167  fun mk_incl_lsbis_tac ctxt n i lsbis_def =
  16.168    EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt CollectI,
  16.169 -    REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, atac, rtac ctxt equalityD2,
  16.170 -    rtac ctxt (mk_nth_conv n i)] 1;
  16.171 +    REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
  16.172 +    rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1;
  16.173  
  16.174  fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
  16.175    EVERY' [rtac ctxt (@{thm equiv_def} RS iffD2),
  16.176  
  16.177      rtac ctxt conjI, rtac ctxt (@{thm refl_on_def} RS iffD2),
  16.178      rtac ctxt conjI, rtac ctxt lsbis_incl, rtac ctxt ballI, rtac ctxt set_mp,
  16.179 -    rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, atac, etac ctxt @{thm Id_onI},
  16.180 +    rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI},
  16.181  
  16.182      rtac ctxt conjI, rtac ctxt (@{thm sym_def} RS iffD2),
  16.183      rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt set_mp,
  16.184 @@ -351,7 +355,7 @@
  16.185      rtac ctxt (@{thm trans_def} RS iffD2),
  16.186      rtac ctxt allI, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt impI, rtac ctxt set_mp,
  16.187      rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis,
  16.188 -    etac ctxt @{thm relcompI}, atac] 1;
  16.189 +    etac ctxt @{thm relcompI}, assume_tac ctxt] 1;
  16.190  
  16.191  fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
  16.192    let
  16.193 @@ -369,20 +373,20 @@
  16.194              etac ctxt equalityD1, etac ctxt CollectD,
  16.195            rtac ctxt ballI,
  16.196              CONJ_WRAP' (fn i => EVERY' [rtac ctxt ballI, etac ctxt CollectE, dtac ctxt @{thm ShiftD},
  16.197 -              dtac ctxt bspec, etac ctxt thin_rl, atac, dtac ctxt (mk_conjunctN n i),
  16.198 +              dtac ctxt bspec, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
  16.199                dtac ctxt bspec, rtac ctxt CollectI, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
  16.200                REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
  16.201                rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
  16.202 -              rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
  16.203 +              rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt,
  16.204                CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
  16.205                  rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
  16.206                  rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
  16.207 -          dtac ctxt bspec, atac, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec,
  16.208 -          etac ctxt @{thm set_mp[OF equalityD1]}, atac,
  16.209 +          dtac ctxt bspec, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec,
  16.210 +          etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt,
  16.211            REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
  16.212            rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
  16.213            etac ctxt (@{thm append_Nil} RS sym RS arg_cong RS trans),
  16.214 -          REPEAT_DETERM_N m o (rtac ctxt conjI THEN' atac),
  16.215 +          REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
  16.216            CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
  16.217              rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
  16.218              rtac ctxt (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
  16.219 @@ -408,12 +412,13 @@
  16.220              (fn i =>
  16.221                EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
  16.222                  rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]},
  16.223 -                REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i), etac ctxt mp, atac]) ks])
  16.224 +                REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
  16.225 +                etac ctxt mp, assume_tac ctxt]) ks])
  16.226        Lev_Sucs] 1
  16.227    end;
  16.228  
  16.229  fun mk_length_Lev'_tac ctxt length_Lev =
  16.230 -  EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, atac] 1;
  16.231 +  EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, assume_tac ctxt] 1;
  16.232  
  16.233  fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss =
  16.234    let
  16.235 @@ -434,7 +439,7 @@
  16.236            CONJ_WRAP' (fn i' => EVERY' [dtac ctxt (mk_conjunctN n i'), etac ctxt exE, rtac ctxt exI,
  16.237              rtac ctxt (@{thm append_Cons} RS arg_cong RS trans), rtac ctxt (rv_Cons RS trans),
  16.238              if n = 1 then K all_tac else etac ctxt (sum_case_cong_weak RS trans),
  16.239 -            rtac ctxt (mk_sum_caseN n i RS trans), atac])
  16.240 +            rtac ctxt (mk_sum_caseN n i RS trans), assume_tac ctxt])
  16.241            ks])
  16.242          rv_Conss)
  16.243        ks)] 1
  16.244 @@ -474,12 +479,12 @@
  16.245                      EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS equalityD2 RS set_mp),
  16.246                        rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i),
  16.247                        rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
  16.248 -                      rtac ctxt conjI, atac, dtac ctxt (sym RS trans RS sym),
  16.249 +                      rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym),
  16.250                        rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans),
  16.251                        etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE,
  16.252 -                      dtac ctxt (mk_conjunctN n i), dtac ctxt mp, atac,
  16.253 -                      dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, atac,
  16.254 -                      dtac ctxt (mk_conjunctN n i''), etac ctxt mp, atac])
  16.255 +                      dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
  16.256 +                      dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
  16.257 +                      dtac ctxt (mk_conjunctN n i''), etac ctxt mp, assume_tac ctxt])
  16.258                    ks)
  16.259                  ks])
  16.260            (rev (ks ~~ from_to_sbds))])
  16.261 @@ -528,14 +533,14 @@
  16.262                    (if k = i
  16.263                    then EVERY' [dtac ctxt (mk_InN_inject n i),
  16.264                      dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
  16.265 -                    atac, atac, hyp_subst_tac ctxt] THEN'
  16.266 +                    assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt] THEN'
  16.267                      CONJ_WRAP' (fn i'' =>
  16.268                        EVERY' [rtac ctxt impI, dtac ctxt (sym RS trans),
  16.269                          rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS arg_cong RS trans),
  16.270                          etac ctxt (from_to_sbd RS arg_cong),
  16.271                          REPEAT_DETERM o etac ctxt allE,
  16.272 -                        dtac ctxt (mk_conjunctN n i), dtac ctxt mp, atac,
  16.273 -                        dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, atac,
  16.274 +                        dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
  16.275 +                        dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
  16.276                          dtac ctxt (mk_conjunctN n i''), etac ctxt mp, etac ctxt sym])
  16.277                      ks
  16.278                    else etac ctxt (mk_InN_not_InM i k RS notE)))
  16.279 @@ -572,13 +577,13 @@
  16.280                CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
  16.281                  EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
  16.282                    rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, etac ctxt set_Lev,
  16.283 -                  if n = 1 then rtac ctxt refl else atac, atac, rtac ctxt subsetI,
  16.284 +                  if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt subsetI,
  16.285                    REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
  16.286                    REPEAT_DETERM_N 4 o etac ctxt thin_rl,
  16.287                    rtac ctxt set_image_Lev,
  16.288 -                  atac, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
  16.289 +                  assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
  16.290                    etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
  16.291 -                  if n = 1 then rtac ctxt refl else atac])
  16.292 +                  if n = 1 then rtac ctxt refl else assume_tac ctxt])
  16.293                (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
  16.294            (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
  16.295              (set_Levss ~~ set_image_Levss))))),
  16.296 @@ -591,7 +596,7 @@
  16.297              EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
  16.298                rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt set_Lev,
  16.299                rtac ctxt (Lev_0 RS equalityD2 RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
  16.300 -              atac, rtac ctxt subsetI,
  16.301 +              assume_tac ctxt, rtac ctxt subsetI,
  16.302                REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
  16.303                rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
  16.304                rtac ctxt @{thm singletonI}, dtac ctxt length_Lev',
  16.305 @@ -621,12 +626,12 @@
  16.306                  dtac ctxt list_inject_iffD1, etac ctxt conjE,
  16.307                  if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'),
  16.308                    dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
  16.309 -                  atac, atac, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
  16.310 +                  assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
  16.311                  else etac ctxt (mk_InN_not_InM i' i'' RS notE)])
  16.312              (rev ks),
  16.313              rtac ctxt @{thm UN_least}, rtac ctxt subsetI, rtac ctxt CollectI, rtac ctxt @{thm UN_I[OF UNIV_I]},
  16.314              rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt CollectI,
  16.315 -            REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, atac,
  16.316 +            REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt,
  16.317              rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI,
  16.318              CONVERSION (Conv.top_conv
  16.319                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
  16.320 @@ -653,7 +658,7 @@
  16.321      etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
  16.322      rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
  16.323      EVERY' (map (fn equiv_LSBIS =>
  16.324 -      EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, atac])
  16.325 +      EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, assume_tac ctxt])
  16.326      equiv_LSBISs), rtac ctxt sym, rtac ctxt (o_apply RS trans),
  16.327      etac ctxt (sym RS arg_cong RS trans), rtac ctxt map_comp_id] 1;
  16.328  
  16.329 @@ -673,11 +678,12 @@
  16.330  fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs =
  16.331    EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI,
  16.332      CONJ_WRAP' (fn equiv_LSBIS =>
  16.333 -      EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff}, rtac ctxt equiv_LSBIS, atac])
  16.334 +      EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
  16.335 +        rtac ctxt equiv_LSBIS, assume_tac ctxt])
  16.336      equiv_LSBISs,
  16.337      CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
  16.338        EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
  16.339 -        rtac ctxt congruent_str_final, atac, rtac ctxt o_apply])
  16.340 +        rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply])
  16.341      (equiv_LSBISs ~~ congruent_str_finals)] 1;
  16.342  
  16.343  fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
  16.344 @@ -716,7 +722,8 @@
  16.345    in
  16.346      EVERY' [rtac ctxt rev_mp, ftac ctxt (bis_def RS iffD1),
  16.347        REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse,
  16.348 -      rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, atac, rtac ctxt bis_Gr, rtac ctxt tcoalg,
  16.349 +      rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt,
  16.350 +      rtac ctxt bis_Gr, rtac ctxt tcoalg,
  16.351        rtac ctxt mor_Rep, REPEAT_DETERM_N n o etac ctxt @{thm relImage_Gr},
  16.352        rtac ctxt impI, rtac ctxt rev_mp, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_Gr, rtac ctxt coalgT,
  16.353        rtac ctxt mor_T_final, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt bis_converse, rtac ctxt bis_Gr, rtac ctxt coalgT,
  16.354 @@ -728,7 +735,7 @@
  16.355            rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]},
  16.356            rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong},
  16.357            rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl,
  16.358 -          rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, atac,
  16.359 +          rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
  16.360            rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on},
  16.361            rtac ctxt Rep_inject])
  16.362        (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
  16.363 @@ -787,7 +794,7 @@
  16.364        EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
  16.365          EVERY' [rtac ctxt subsetI, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
  16.366            etac ctxt UnE, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt UnE,
  16.367 -          EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, atac]) set_Jset_Jsets)])
  16.368 +          EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)])
  16.369        (1 upto n) set_Jsets set_Jset_Jsetss)] 1;
  16.370  
  16.371  fun mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets =
  16.372 @@ -840,7 +847,7 @@
  16.373               rtac ctxt CollectI, etac ctxt CollectE,
  16.374               REPEAT_DETERM o etac ctxt conjE,
  16.375               CONJ_WRAP' (fn set_Jset_Jset =>
  16.376 -               EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, atac]) set_Jset_Jsets,
  16.377 +               EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
  16.378               rtac ctxt (conjI OF [refl, refl])])
  16.379             (drop m set_map0s ~~ set_Jset_Jsetss)])
  16.380          (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
  16.381 @@ -912,7 +919,7 @@
  16.382  
  16.383  fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
  16.384    ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN
  16.385 -  REPEAT_DETERM (atac 1 ORELSE
  16.386 +  REPEAT_DETERM (assume_tac ctxt 1 ORELSE
  16.387      EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
  16.388      K (unfold_thms_tac ctxt dtor_ctors),
  16.389      REPEAT_DETERM_N n o etac ctxt UnE,
  16.390 @@ -966,14 +973,14 @@
  16.391          CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
  16.392            EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
  16.393              rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
  16.394 -            CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
  16.395 +            CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls,
  16.396              rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
  16.397          (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
  16.398          CONJ_WRAP' (fn conv =>
  16.399            EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
  16.400            REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
  16.401            REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]),
  16.402 -          rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), atac])
  16.403 +          rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt])
  16.404          @{thms fst_conv snd_conv}];
  16.405      val only_if_tac =
  16.406        EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
  16.407 @@ -981,7 +988,7 @@
  16.408          CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
  16.409            EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least},
  16.410              rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0,
  16.411 -            rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans_fun_cong_image_id_id_apply, atac,
  16.412 +            rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt,
  16.413              CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
  16.414                (fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans,
  16.415                  rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
  16.416 @@ -993,20 +1000,20 @@
  16.417                  hyp_subst_tac ctxt,
  16.418                  dtac ctxt (in_Jrel RS iffD1),
  16.419                  dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
  16.420 -                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], atac])
  16.421 +                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
  16.422              (rev (active_set_map0s ~~ in_Jrels))])
  16.423          (dtor_sets ~~ passive_set_map0s),
  16.424          rtac ctxt conjI,
  16.425          REPEAT_DETERM_N 2 o EVERY'[rtac ctxt (dtor_inject RS iffD1), rtac ctxt trans, rtac ctxt dtor_map,
  16.426            rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans,
  16.427            rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
  16.428 -          EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, atac,
  16.429 +          EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
  16.430              dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
  16.431              REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
  16.432                @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
  16.433              hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
  16.434 -            dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, atac]) in_Jrels),
  16.435 -          atac]]
  16.436 +            dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels),
  16.437 +          assume_tac ctxt]]
  16.438    in
  16.439      EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1
  16.440    end;
  16.441 @@ -1023,7 +1030,7 @@
  16.442            fn dtor_unfold => fn dtor_map => fn in_rel =>
  16.443          EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
  16.444            REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
  16.445 -          select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, atac,
  16.446 +          select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
  16.447            REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
  16.448            rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI,
  16.449            rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym),
  16.450 @@ -1039,8 +1046,8 @@
  16.451            CONJ_WRAP' (fn set_map0 =>
  16.452              EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
  16.453                rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI},
  16.454 -              FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, atac,
  16.455 -                rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
  16.456 +              FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp,
  16.457 +                assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
  16.458            set_map0s])
  16.459        ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1
  16.460    end;
  16.461 @@ -1053,7 +1060,7 @@
  16.462      rtac ctxt set_induct 1 THEN
  16.463      EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
  16.464        EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
  16.465 -        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, atac,
  16.466 +        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
  16.467          REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
  16.468          hyp_subst_tac ctxt,
  16.469          SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
  16.470 @@ -1062,11 +1069,12 @@
  16.471      EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
  16.472        EVERY' (map (fn set_map0 =>
  16.473          EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
  16.474 -        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, atac,
  16.475 +        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
  16.476          REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
  16.477          SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
  16.478          etac ctxt imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
  16.479 -        rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, atac, rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
  16.480 +        rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt,
  16.481 +        rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
  16.482        (drop m set_map0s)))
  16.483      unfolds set_map0ss ks) 1
  16.484    end;
  16.485 @@ -1082,16 +1090,18 @@
  16.486          if null helper_inds then rtac ctxt UNIV_I
  16.487          else rtac ctxt CollectI THEN'
  16.488            CONJ_WRAP' (fn helper_ind =>
  16.489 -            EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o atac,
  16.490 +            EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
  16.491                REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI,
  16.492                REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
  16.493 -              dtac ctxt bspec, atac, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
  16.494 +              dtac ctxt bspec, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
  16.495                etac ctxt (refl RSN (2, conjI))])
  16.496            helper_inds,
  16.497          rtac ctxt conjI,
  16.498 -        rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac ctxt thin_rl,
  16.499 +        rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
  16.500 +        REPEAT_DETERM_N n o etac ctxt thin_rl,
  16.501          rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI)),
  16.502 -        rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac ctxt thin_rl,
  16.503 +        rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
  16.504 +        REPEAT_DETERM_N n o etac ctxt thin_rl,
  16.505          rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI))])
  16.506      (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
  16.507    end;
    17.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    17.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    17.3 @@ -92,7 +92,7 @@
    17.4  
    17.5  fun mk_alg_set_tac ctxt alg_def =
    17.6    EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI,
    17.7 -   REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), atac] 1;
    17.8 +   REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1;
    17.9  
   17.10  fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
   17.11    (EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
   17.12 @@ -100,7 +100,7 @@
   17.13      [EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits],
   17.14      EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits],
   17.15      EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
   17.16 -      FIRST' (map (fn thm => rtac ctxt thm THEN' atac) alg_sets)]] THEN'
   17.17 +      FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN'
   17.18    etac ctxt @{thm emptyE}) 1;
   17.19  
   17.20  fun mk_mor_elim_tac ctxt mor_def =
   17.21 @@ -108,7 +108,7 @@
   17.22    REPEAT o etac ctxt conjE THEN'
   17.23    TRY o rtac ctxt @{thm image_subsetI} THEN'
   17.24    etac ctxt bspec THEN'
   17.25 -  atac) 1;
   17.26 +  assume_tac ctxt) 1;
   17.27  
   17.28  fun mk_mor_incl_tac ctxt mor_def map_ids =
   17.29    (rtac ctxt (mor_def RS iffD2) THEN'
   17.30 @@ -121,15 +121,16 @@
   17.31  fun mk_mor_comp_tac ctxt mor_def set_maps map_comp_ids =
   17.32    let
   17.33      val fbetw_tac =
   17.34 -      EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt bspec, etac ctxt bspec, atac];
   17.35 +      EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}),
   17.36 +        etac ctxt bspec, etac ctxt bspec, assume_tac ctxt];
   17.37      fun mor_tac (set_map, map_comp_id) =
   17.38        EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
   17.39 -        rtac ctxt trans, dtac ctxt rev_bspec, atac, etac ctxt arg_cong,
   17.40 +        rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
   17.41           REPEAT o eresolve0_tac [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
   17.42        CONJ_WRAP' (fn thm =>
   17.43          FIRST' [rtac ctxt subset_UNIV,
   17.44            (EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
   17.45 -            etac ctxt bspec, etac ctxt set_mp, atac])]) set_map THEN'
   17.46 +            etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
   17.47        rtac ctxt (map_comp_id RS arg_cong);
   17.48    in
   17.49      (dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN'
   17.50 @@ -195,11 +196,12 @@
   17.51      CONJ_WRAP' (fn i =>
   17.52        EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
   17.53        (0 upto n - 1),
   17.54 -    atac] 1;
   17.55 +    assume_tac ctxt] 1;
   17.56  
   17.57  fun mk_min_algs_tac ctxt worel in_congs =
   17.58    let
   17.59 -    val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec, atac, etac ctxt arg_cong];
   17.60 +    val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec,
   17.61 +      assume_tac ctxt, etac ctxt arg_cong];
   17.62      fun minH_tac thm =
   17.63        EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm,
   17.64          REPEAT_DETERM_N (length in_congs) o minG_tac, rtac ctxt refl];
   17.65 @@ -212,8 +214,9 @@
   17.66  
   17.67  fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
   17.68    rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI,
   17.69 -  rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, atac, atac, rtac ctxt equalityD1,
   17.70 -  dtac ctxt @{thm notnotD}, hyp_subst_tac ctxt, rtac ctxt refl] 1;
   17.71 +  rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
   17.72 +  assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD},
   17.73 +  hyp_subst_tac ctxt, rtac ctxt refl] 1;
   17.74  
   17.75  fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
   17.76    suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
   17.77 @@ -236,8 +239,10 @@
   17.78  
   17.79      val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq},
   17.80        rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order,
   17.81 -      atac, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
   17.82 -      dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT o etac ctxt conjE, atac, rtac ctxt Asuc_Cinfinite]
   17.83 +      assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE,
   17.84 +      dtac ctxt mp, etac ctxt @{thm underS_E},
   17.85 +      dtac ctxt mp, etac ctxt @{thm underS_Field},
   17.86 +      REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite]
   17.87  
   17.88      fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans},
   17.89        rtac ctxt @{thm card_of_ordIso_subst}, etac ctxt min_alg, rtac ctxt @{thm Un_Cinfinite_bound},
   17.90 @@ -265,8 +270,9 @@
   17.91      val induct = worel RS
   17.92        Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   17.93  
   17.94 -    val minG_tac = EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
   17.95 -      dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, atac];
   17.96 +    val minG_tac =
   17.97 +      EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
   17.98 +        dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt];
   17.99  
  17.100      fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
  17.101        rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
  17.102 @@ -288,15 +294,17 @@
  17.103      fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
  17.104        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
  17.105          EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
  17.106 -        rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, atac,
  17.107 +        rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
  17.108          rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
  17.109 -        rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl, atac, rtac ctxt set_mp,
  17.110 -        rtac ctxt equalityD2, rtac ctxt min_alg, atac, rtac ctxt UnI2, rtac ctxt @{thm image_eqI}, rtac ctxt refl,
  17.111 +        rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl,
  17.112 +        assume_tac ctxt, rtac ctxt set_mp,
  17.113 +        rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2,
  17.114 +        rtac ctxt @{thm image_eqI}, rtac ctxt refl,
  17.115          rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
  17.116          REPEAT_DETERM o etac ctxt conjE,
  17.117 -        CONJ_WRAP' (K (FIRST' [atac,
  17.118 +        CONJ_WRAP' (K (FIRST' [assume_tac ctxt,
  17.119            EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I},
  17.120 -            etac ctxt @{thm underS_I}, atac, atac]]))
  17.121 +            etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]]))
  17.122            set_bds];
  17.123    in
  17.124      (rtac ctxt (alg_def RS iffD2) THEN'
  17.125 @@ -307,24 +315,27 @@
  17.126    EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}),
  17.127      rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans},
  17.128      rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq},
  17.129 -    rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of,  REPEAT_DETERM o etac ctxt conjE, atac,
  17.130 -    rtac ctxt Asuc_Cinfinite] 1;
  17.131 +    rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of,
  17.132 +    REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1;
  17.133  
  17.134  fun mk_least_min_alg_tac ctxt min_alg_def least =
  17.135 -  EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least}, dtac ctxt least, dtac ctxt mp, atac,
  17.136 -    REPEAT_DETERM o etac ctxt conjE, atac] 1;
  17.137 +  EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least},
  17.138 +    dtac ctxt least, dtac ctxt mp, assume_tac ctxt,
  17.139 +    REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1;
  17.140  
  17.141  fun mk_alg_select_tac ctxt Abs_inverse =
  17.142    EVERY' [rtac ctxt ballI,
  17.143      REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
  17.144 -  unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
  17.145 +  unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1;
  17.146  
  17.147  fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
  17.148      set_maps str_init_defs =
  17.149    let
  17.150      val n = length alg_sets;
  17.151      val fbetw_tac =
  17.152 -      CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec, etac ctxt CollectE, atac])) alg_sets;
  17.153 +      CONJ_WRAP'
  17.154 +        (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec,
  17.155 +          etac ctxt CollectE, assume_tac ctxt])) alg_sets;
  17.156      val mor_tac =
  17.157        CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
  17.158      fun alg_epi_tac ((alg_set, str_init_def), set_map) =
  17.159 @@ -332,7 +343,7 @@
  17.160          rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}),
  17.161          etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve0_tac set_map,
  17.162            rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
  17.163 -          atac]];
  17.164 +          assume_tac ctxt]];
  17.165    in
  17.166      EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}),
  17.167        rtac ctxt (Thm.permute_prems 0 1 mor_comp), etac ctxt (Thm.permute_prems 0 1 mor_comp),
  17.168 @@ -345,10 +356,11 @@
  17.169      val n = length card_of_min_algs;
  17.170    in
  17.171      EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
  17.172 -      REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy, REPEAT_DETERM_N n o atac,
  17.173 +      REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy,
  17.174 +      REPEAT_DETERM_N n o assume_tac ctxt,
  17.175        rtac ctxt impI, REPEAT_DETERM o eresolve0_tac [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
  17.176        rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
  17.177 -      rtac ctxt conjI, rtac ctxt refl, atac,
  17.178 +      rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
  17.179        SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
  17.180        etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1
  17.181    end;
  17.182 @@ -361,11 +373,11 @@
  17.183  
  17.184      fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono,
  17.185        REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
  17.186 -      REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' atac)];
  17.187 +      REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
  17.188      fun cong_tac ct map_cong0 = EVERY'
  17.189        [rtac ctxt (map_cong0 RS cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong),
  17.190        REPEAT_DETERM_N m o rtac ctxt refl,
  17.191 -      REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' atac)];
  17.192 +      REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
  17.193  
  17.194      fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
  17.195        EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
  17.196 @@ -391,9 +403,10 @@
  17.197        REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
  17.198        REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
  17.199        rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
  17.200 -      REPEAT_DETERM_N m o (rtac ctxt conjI THEN' atac),
  17.201 +      REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
  17.202        CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets,
  17.203 -      CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' atac)) alg_sets];
  17.204 +      CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
  17.205 +        alg_sets];
  17.206  
  17.207      fun mk_induct_tac least_min_alg =
  17.208        rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
  17.209 @@ -422,7 +435,8 @@
  17.210        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
  17.211          rtac ctxt (thm RS (cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong) RS sym),
  17.212          EVERY' (map (fn Abs_inverse =>
  17.213 -          EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse), atac])
  17.214 +          EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
  17.215 +            assume_tac ctxt])
  17.216          Abs_inverses)])
  17.217      (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
  17.218  
  17.219 @@ -436,8 +450,8 @@
  17.220      fun mk_unique type_def =
  17.221        EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
  17.222          rtac ctxt ballI, resolve0_tac init_unique_mors,
  17.223 -        EVERY' (map (fn thm => atac ORELSE' rtac ctxt thm) Reps),
  17.224 -        rtac ctxt mor_comp, rtac ctxt mor_Abs, atac,
  17.225 +        EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
  17.226 +        rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
  17.227          rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
  17.228    in
  17.229      CONJ_WRAP' mk_unique type_defs 1
  17.230 @@ -469,13 +483,14 @@
  17.231      fun mk_IH_tac Rep_inv Abs_inv set_map =
  17.232        DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec,
  17.233          dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE,
  17.234 -        hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp, atac, atac];
  17.235 +        hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp,
  17.236 +        assume_tac ctxt, assume_tac ctxt];
  17.237  
  17.238      fun mk_closed_tac (k, (morE, set_maps)) =
  17.239        EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI,
  17.240 -        rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), atac,
  17.241 +        rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt,
  17.242          REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec},
  17.243 -        EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
  17.244 +        EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt];
  17.245  
  17.246      fun mk_induct_tac (Rep, Rep_inv) =
  17.247        EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))];
  17.248 @@ -495,13 +510,14 @@
  17.249          select_prem_tac ctxt n (dtac ctxt @{thm meta_spec2}) i,
  17.250          REPEAT_DETERM_N n o
  17.251            EVERY' [dtac ctxt meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
  17.252 -            REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp), atac],
  17.253 -        atac];
  17.254 +            REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp),
  17.255 +            assume_tac ctxt],
  17.256 +        assume_tac ctxt];
  17.257    in
  17.258      EVERY' [rtac ctxt rev_mp, rtac ctxt (Drule.instantiate' cTs cts ctor_induct),
  17.259        EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI,
  17.260        REPEAT_DETERM o eresolve_tac ctxt [conjE, allE],
  17.261 -      CONJ_WRAP' (K atac) ks] 1
  17.262 +      CONJ_WRAP' (K (assume_tac ctxt)) ks] 1
  17.263    end;
  17.264  
  17.265  fun mk_map_tac ctxt m n foldx map_comp_id map_cong0 =
  17.266 @@ -515,7 +531,7 @@
  17.267  fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
  17.268    rtac ctxt fold_unique 1 THEN
  17.269    unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
  17.270 -  ALLGOALS atac;
  17.271 +  ALLGOALS (assume_tac ctxt);
  17.272  
  17.273  fun mk_set_tac ctxt foldx = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply,
  17.274    rtac ctxt trans, rtac ctxt foldx, rtac ctxt sym, rtac ctxt o_apply] 1;
  17.275 @@ -592,8 +608,8 @@
  17.276      EVERY' [rtac ctxt impI, etac ctxt (nchotomy RS @{thm nchotomy_relcomppE}),
  17.277        REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2),
  17.278        rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}),
  17.279 -      rtac ctxt @{thm relcomppI}, atac, atac,
  17.280 -      REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, atac],
  17.281 +      rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt,
  17.282 +      REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt],
  17.283        REPEAT_DETERM_N (length le_rel_OOs) o
  17.284          EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]])
  17.285    ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
  17.286 @@ -627,7 +643,7 @@
  17.287    CONJ_WRAP_GEN' (rtac ctxt @{thm card_order_csum}) (rtac ctxt) bd_card_orders 1;
  17.288  
  17.289  fun mk_wit_tac ctxt n ctor_set wit =
  17.290 -  REPEAT_DETERM (atac 1 ORELSE
  17.291 +  REPEAT_DETERM (assume_tac ctxt 1 ORELSE
  17.292      EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
  17.293      REPEAT_DETERM o
  17.294        (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
  17.295 @@ -676,7 +692,7 @@
  17.296          CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
  17.297            EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least},
  17.298              rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]},
  17.299 -            rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, atac,
  17.300 +            rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt,
  17.301              CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
  17.302                (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
  17.303                  rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
  17.304 @@ -686,21 +702,23 @@
  17.305                    @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
  17.306                  hyp_subst_tac ctxt,
  17.307                  dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
  17.308 -                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], atac])
  17.309 +                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
  17.310              (rev (active_set_map0s ~~ in_Irels))])
  17.311          (ctor_sets ~~ passive_set_map0s),
  17.312          rtac ctxt conjI,
  17.313          REPEAT_DETERM_N 2 o EVERY' [rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt (ctor_inject RS iffD2),
  17.314            rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
  17.315            REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
  17.316 -          EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, atac,
  17.317 +          EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
  17.318 +            dtac ctxt set_rev_mp, assume_tac ctxt,
  17.319              dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
  17.320              REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
  17.321                @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
  17.322              hyp_subst_tac ctxt,
  17.323 -            dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, atac])
  17.324 +            dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex},
  17.325 +            REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])
  17.326            in_Irels),
  17.327 -          atac]]
  17.328 +          assume_tac ctxt]]
  17.329    in
  17.330      EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1
  17.331    end;
  17.332 @@ -753,7 +771,7 @@
  17.333          rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
  17.334          REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer},
  17.335          REPEAT_DETERM_N n o rtac ctxt @{thm vimage2p_rel_fun},
  17.336 -        atac])
  17.337 +        assume_tac ctxt])
  17.338        map_transfers)])
  17.339    end;
  17.340  
    18.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    18.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    18.3 @@ -100,7 +100,8 @@
    18.4  
    18.5  fun mk_map_cong0L_tac ctxt passive map_cong0 map_id =
    18.6    (rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN
    18.7 -  REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt bspec, atac, rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN
    18.8 +  REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt bspec, assume_tac ctxt,
    18.9 +      rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN
   18.10    rtac ctxt map_id 1;
   18.11  
   18.12  end;
    19.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Jul 18 20:37:16 2015 +0200
    19.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Jul 18 20:47:08 2015 +0200
    19.3 @@ -54,17 +54,21 @@
    19.4  
    19.5  fun mk_nchotomy_tac ctxt n exhaust =
    19.6    HEADGOAL (rtac ctxt allI THEN' rtac ctxt exhaust THEN'
    19.7 -    EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, atac]) (1 upto n)));
    19.8 +    EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
    19.9 +      (1 upto n)));
   19.10  
   19.11  fun mk_unique_disc_def_tac ctxt m uexhaust =
   19.12 -  HEADGOAL (EVERY' [rtac ctxt iffI, rtac ctxt uexhaust, REPEAT_DETERM_N m o rtac ctxt exI, atac, rtac ctxt refl]);
   19.13 +  HEADGOAL (EVERY'
   19.14 +    [rtac ctxt iffI, rtac ctxt uexhaust, REPEAT_DETERM_N m o rtac ctxt exI,
   19.15 +      assume_tac ctxt, rtac ctxt refl]);
   19.16  
   19.17  fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
   19.18    HEADGOAL (EVERY' ([rtac ctxt (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
   19.19      rtac ctxt @{thm iffI_np}, REPEAT_DETERM o etac ctxt exE,
   19.20      hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac ctxt allI,
   19.21      rtac ctxt distinct, rtac ctxt uexhaust] @
   19.22 -    (([etac ctxt notE, REPEAT_DETERM o rtac ctxt exI, atac], [REPEAT_DETERM o rtac ctxt exI, atac])
   19.23 +    (([etac ctxt notE, REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt],
   19.24 +      [REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
   19.25       |> k = 1 ? swap |> op @)));
   19.26  
   19.27  fun mk_half_distinct_disc_tac ctxt m discD disc' =
   19.28 @@ -77,7 +81,7 @@
   19.29  fun mk_exhaust_disc_or_sel_tac ctxt n exhaust destIs =
   19.30    HEADGOAL (rtac ctxt exhaust THEN'
   19.31      EVERY' (map2 (fn k => fn destI => dtac ctxt destI THEN'
   19.32 -      select_prem_tac ctxt n (etac ctxt meta_mp) k THEN' atac) (1 upto n) destIs));
   19.33 +      select_prem_tac ctxt n (etac ctxt meta_mp) k THEN' assume_tac ctxt) (1 upto n) destIs));
   19.34  
   19.35  val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac;
   19.36  
   19.37 @@ -88,7 +92,7 @@
   19.38  fun mk_collapse_tac ctxt m discD sels =
   19.39    HEADGOAL (dtac ctxt discD THEN'
   19.40      (if m = 0 then
   19.41 -       atac
   19.42 +       assume_tac ctxt
   19.43       else
   19.44         REPEAT_DETERM_N m o etac ctxt exE THEN' hyp_subst_tac ctxt THEN'
   19.45         SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac ctxt refl));
   19.46 @@ -105,26 +109,29 @@
   19.47      distinct_discsss' =
   19.48    if ms = [0] then
   19.49      HEADGOAL (rtac ctxt (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
   19.50 -      TRY o EVERY' [rtac ctxt uexhaust_disc, atac, rtac ctxt vexhaust_disc, atac])
   19.51 +      TRY o
   19.52 +      EVERY' [rtac ctxt uexhaust_disc, assume_tac ctxt, rtac ctxt vexhaust_disc, assume_tac ctxt])
   19.53    else
   19.54      let val ks = 1 upto n in
   19.55        HEADGOAL (rtac ctxt uexhaust_disc THEN'
   19.56          EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
   19.57 -          EVERY' [rtac ctxt (uuncollapse RS trans) THEN' TRY o atac, rtac ctxt sym, rtac ctxt vexhaust_disc,
   19.58 +          EVERY' [rtac ctxt (uuncollapse RS trans) THEN'
   19.59 +            TRY o assume_tac ctxt, rtac ctxt sym, rtac ctxt vexhaust_disc,
   19.60              EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
   19.61                EVERY'
   19.62                  (if k' = k then
   19.63 -                   [rtac ctxt (vuncollapse RS trans), TRY o atac] @
   19.64 +                   [rtac ctxt (vuncollapse RS trans), TRY o assume_tac ctxt] @
   19.65                     (if m = 0 then
   19.66                        [rtac ctxt refl]
   19.67                      else
   19.68 -                      [if n = 1 then K all_tac else EVERY' [dtac ctxt meta_mp, atac, dtac ctxt meta_mp, atac],
   19.69 +                      [if n = 1 then K all_tac
   19.70 +                       else EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp, assume_tac ctxt],
   19.71                         REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE,
   19.72                         asm_simp_tac (ss_only [] ctxt)])
   19.73                   else
   19.74                     [dtac ctxt (the_single (if k = n then distinct_discs else distinct_discs')),
   19.75                      etac ctxt (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
   19.76 -                    atac, atac]))
   19.77 +                    assume_tac ctxt, assume_tac ctxt]))
   19.78                ks distinct_discss distinct_discss' uncollapses)])
   19.79            ks ms distinct_discsss distinct_discsss' uncollapses))
   19.80      end;
   19.81 @@ -132,7 +139,7 @@
   19.82  fun mk_case_same_ctr_tac ctxt injects =
   19.83    REPEAT_DETERM o etac ctxt exE THEN' etac ctxt conjE THEN'
   19.84      (case injects of
   19.85 -      [] => atac
   19.86 +      [] => assume_tac ctxt
   19.87      | [inject] => dtac ctxt (inject RS iffD1) THEN' REPEAT_DETERM o etac ctxt conjE THEN'
   19.88          hyp_subst_tac ctxt THEN' rtac ctxt refl);
   19.89  
   19.90 @@ -176,8 +183,10 @@
   19.91           flat (nth distinctsss (k - 1))) ctxt)) k) THEN
   19.92      ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN'
   19.93        REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN' REPEAT_DETERM o etac ctxt conjE THEN'
   19.94 -      hyp_subst_tac ctxt THEN' atac THEN' REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
   19.95 -      REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN' rtac ctxt refl THEN' atac)
   19.96 +      hyp_subst_tac ctxt THEN' assume_tac ctxt THEN'
   19.97 +      REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
   19.98 +      REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'
   19.99 +      rtac ctxt refl THEN' assume_tac ctxt)
  19.100    end;
  19.101  
  19.102  val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
    20.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Jul 18 20:37:16 2015 +0200
    20.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sat Jul 18 20:47:08 2015 +0200
    20.3 @@ -275,8 +275,8 @@
    20.4    let val (butlast, last) = split_last xs;
    20.5    in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
    20.6  
    20.7 -fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
    20.8 -fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
    20.9 +fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (resolve0_tac [conjI] 1) gen_tac;
   20.10 +fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (resolve0_tac [conjI]) gen_tac;
   20.11  
   20.12  fun rtac ctxt thm = resolve_tac ctxt [thm];
   20.13  fun etac ctxt thm = eresolve_tac ctxt [thm];
    21.1 --- a/src/HOL/Tools/Function/function_core.ML	Sat Jul 18 20:37:16 2015 +0200
    21.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sat Jul 18 20:47:08 2015 +0200
    21.3 @@ -692,7 +692,7 @@
    21.4        subset_induct_rule
    21.5        |> Thm.forall_intr (Thm.cterm_of ctxt D)
    21.6        |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
    21.7 -      |> atac 1 |> Seq.hd
    21.8 +      |> assume_tac ctxt 1 |> Seq.hd
    21.9        |> (curry op COMP) (acc_downward
   21.10          |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
   21.11          |> Thm.forall_intr (Thm.cterm_of ctxt z)
    22.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 18 20:37:16 2015 +0200
    22.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 18 20:47:08 2015 +0200
    22.3 @@ -104,17 +104,17 @@
    22.4  
    22.5  (** Proof Reconstruction **)
    22.6  
    22.7 -fun prove_row (c :: cs) =
    22.8 -  (case Lazy.force c of
    22.9 -     Less thm =>
   22.10 -       rtac @{thm "mlex_less"} 1
   22.11 -       THEN PRIMITIVE (Thm.elim_implies thm)
   22.12 -   | LessEq (thm, _) =>
   22.13 -       rtac @{thm "mlex_leq"} 1
   22.14 -       THEN PRIMITIVE (Thm.elim_implies thm)
   22.15 -       THEN prove_row cs
   22.16 -   | _ => raise General.Fail "lexicographic_order")
   22.17 - | prove_row [] = no_tac;
   22.18 +fun prove_row_tac ctxt (c :: cs) =
   22.19 +      (case Lazy.force c of
   22.20 +        Less thm =>
   22.21 +          resolve_tac ctxt @{thms mlex_less} 1
   22.22 +          THEN PRIMITIVE (Thm.elim_implies thm)
   22.23 +      | LessEq (thm, _) =>
   22.24 +          resolve_tac ctxt @{thms mlex_leq} 1
   22.25 +          THEN PRIMITIVE (Thm.elim_implies thm)
   22.26 +          THEN prove_row_tac ctxt cs
   22.27 +      | _ => raise General.Fail "lexicographic_order")
   22.28 +  | prove_row_tac _ [] = no_tac;
   22.29  
   22.30  
   22.31  (** Error reporting **)
   22.32 @@ -202,9 +202,9 @@
   22.33          in (* 4: proof reconstruction *)
   22.34            st |>
   22.35            (PRIMITIVE (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
   22.36 -            THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
   22.37 -            THEN (rtac @{thm "wf_empty"} 1)
   22.38 -            THEN EVERY (map prove_row clean_table))
   22.39 +            THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
   22.40 +            THEN (resolve_tac ctxt @{thms wf_empty} 1)
   22.41 +            THEN EVERY (map (prove_row_tac ctxt) clean_table))
   22.42          end
   22.43    end) 1 st;
   22.44  
    23.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Jul 18 20:37:16 2015 +0200
    23.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Jul 18 20:47:08 2015 +0200
    23.3 @@ -17,9 +17,9 @@
    23.4       msetT : typ -> typ,
    23.5       mk_mset : typ -> term list -> term,
    23.6       mset_regroup_conv : Proof.context -> int list -> conv,
    23.7 -     mset_member_tac : int -> int -> tactic,
    23.8 -     mset_nonempty_tac : int -> tactic,
    23.9 -     mset_pwleq_tac : int -> tactic,
   23.10 +     mset_member_tac : Proof.context -> int -> int -> tactic,
   23.11 +     mset_nonempty_tac : Proof.context -> int -> tactic,
   23.12 +     mset_pwleq_tac : Proof.context -> int -> tactic,
   23.13       set_of_simps : thm list,
   23.14       smsI' : thm,
   23.15       wmsI2'' : thm,
   23.16 @@ -49,9 +49,9 @@
   23.17     msetT : typ -> typ,
   23.18     mk_mset : typ -> term list -> term,
   23.19     mset_regroup_conv : Proof.context -> int list -> conv,
   23.20 -   mset_member_tac : int -> int -> tactic,
   23.21 -   mset_nonempty_tac : int -> tactic,
   23.22 -   mset_pwleq_tac : int -> tactic,
   23.23 +   mset_member_tac : Proof.context -> int -> int -> tactic,
   23.24 +   mset_nonempty_tac : Proof.context -> int -> tactic,
   23.25 +   mset_pwleq_tac : Proof.context -> int -> tactic,
   23.26     set_of_simps : thm list,
   23.27     smsI' : thm,
   23.28     wmsI2'' : thm,
   23.29 @@ -116,13 +116,13 @@
   23.30  
   23.31  (* General reduction pair application *)
   23.32  fun rem_inv_img ctxt =
   23.33 -  rtac @{thm subsetI} 1
   23.34 -  THEN etac @{thm CollectE} 1
   23.35 -  THEN REPEAT (etac @{thm exE} 1)
   23.36 +  resolve_tac ctxt @{thms subsetI} 1
   23.37 +  THEN eresolve_tac ctxt @{thms CollectE} 1
   23.38 +  THEN REPEAT (eresolve_tac ctxt @{thms exE} 1)
   23.39    THEN Local_Defs.unfold_tac ctxt @{thms inv_image_def}
   23.40 -  THEN rtac @{thm CollectI} 1
   23.41 -  THEN etac @{thm conjE} 1
   23.42 -  THEN etac @{thm ssubst} 1
   23.43 +  THEN resolve_tac ctxt @{thms CollectI} 1
   23.44 +  THEN eresolve_tac ctxt @{thms conjE} 1
   23.45 +  THEN eresolve_tac ctxt @{thms ssubst} 1
   23.46    THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
   23.47  
   23.48  
   23.49 @@ -130,15 +130,15 @@
   23.50  
   23.51  val setT = HOLogic.mk_setT
   23.52  
   23.53 -fun set_member_tac m i =
   23.54 -  if m = 0 then rtac @{thm insertI1} i
   23.55 -  else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
   23.56 +fun set_member_tac ctxt m i =
   23.57 +  if m = 0 then resolve_tac ctxt @{thms insertI1} i
   23.58 +  else resolve_tac ctxt @{thms insertI2} i THEN set_member_tac ctxt (m - 1) i
   23.59  
   23.60 -val set_nonempty_tac = rtac @{thm insert_not_empty}
   23.61 +fun set_nonempty_tac ctxt = resolve_tac ctxt @{thms insert_not_empty}
   23.62  
   23.63 -fun set_finite_tac i =
   23.64 -  rtac @{thm finite.emptyI} i
   23.65 -  ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
   23.66 +fun set_finite_tac ctxt i =
   23.67 +  resolve_tac ctxt @{thms finite.emptyI} i
   23.68 +  ORELSE (resolve_tac ctxt @{thms finite.insertI} i THEN (fn st => set_finite_tac ctxt i st))
   23.69  
   23.70  
   23.71  (* Reconstruction *)
   23.72 @@ -183,7 +183,7 @@
   23.73                then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
   23.74                else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
   23.75            in
   23.76 -            rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
   23.77 +            resolve_tac ctxt [rule] 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
   23.78              THEN (if tag_flag then Arith_Data.arith_tac ctxt 1 else all_tac)
   23.79            end
   23.80  
   23.81 @@ -192,16 +192,16 @@
   23.82                  val (empty, step) = ord_intros_max strict
   23.83                in
   23.84                  if length lq = 0
   23.85 -                then rtac empty 1 THEN set_finite_tac 1
   23.86 -                     THEN (if strict then set_nonempty_tac 1 else all_tac)
   23.87 +                then resolve_tac ctxt [empty] 1 THEN set_finite_tac ctxt 1
   23.88 +                     THEN (if strict then set_nonempty_tac ctxt 1 else all_tac)
   23.89                  else
   23.90                    let
   23.91                      val (j, b) :: rest = lq
   23.92                      val (i, a) = the (covering g strict j)
   23.93 -                    fun choose xs = set_member_tac (find_index (curry op = (i, a)) xs) 1
   23.94 +                    fun choose xs = set_member_tac ctxt (find_index (curry op = (i, a)) xs) 1
   23.95                      val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
   23.96                    in
   23.97 -                    rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
   23.98 +                    resolve_tac ctxt [step] 1 THEN solve_tac THEN steps_tac MAX strict rest lp
   23.99                    end
  23.100                end
  23.101            | steps_tac MIN strict lq lp =
  23.102 @@ -209,16 +209,16 @@
  23.103                  val (empty, step) = ord_intros_min strict
  23.104                in
  23.105                  if length lp = 0
  23.106 -                then rtac empty 1
  23.107 -                     THEN (if strict then set_nonempty_tac 1 else all_tac)
  23.108 +                then resolve_tac ctxt [empty] 1
  23.109 +                     THEN (if strict then set_nonempty_tac ctxt 1 else all_tac)
  23.110                  else
  23.111                    let
  23.112                      val (i, a) :: rest = lp
  23.113                      val (j, b) = the (covering g strict i)
  23.114 -                    fun choose xs = set_member_tac (find_index (curry op = (j, b)) xs) 1
  23.115 +                    fun choose xs = set_member_tac ctxt (find_index (curry op = (j, b)) xs) 1
  23.116                      val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
  23.117                    in
  23.118 -                    rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
  23.119 +                    resolve_tac ctxt [step] 1 THEN solve_tac THEN steps_tac MIN strict lq rest
  23.120                    end
  23.121                end
  23.122            | steps_tac MS strict lq lp =
  23.123 @@ -243,10 +243,10 @@
  23.124                  end
  23.125                in
  23.126                  CONVERSION goal_rewrite 1
  23.127 -                THEN (if strict then rtac smsI' 1
  23.128 -                      else if qs = lq then rtac wmsI2'' 1
  23.129 -                      else rtac wmsI1 1)
  23.130 -                THEN mset_pwleq_tac 1
  23.131 +                THEN (if strict then resolve_tac ctxt [smsI'] 1
  23.132 +                      else if qs = lq then resolve_tac ctxt [wmsI2''] 1
  23.133 +                      else resolve_tac ctxt [wmsI1] 1)
  23.134 +                THEN mset_pwleq_tac ctxt 1
  23.135                  THEN EVERY (map2 (less_proof false) qs ps)
  23.136                  THEN (if strict orelse qs <> lq
  23.137                        then Local_Defs.unfold_tac ctxt set_of_simps
  23.138 @@ -275,9 +275,9 @@
  23.139      in
  23.140        PROFILE "Proof Reconstruction"
  23.141          (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv ctxt sl))) 1
  23.142 -         THEN (rtac @{thm reduction_pair_lemma} 1)
  23.143 -         THEN (rtac @{thm rp_inv_image_rp} 1)
  23.144 -         THEN (rtac (order_rpair ms_rp label) 1)
  23.145 +         THEN (resolve_tac ctxt @{thms reduction_pair_lemma} 1)
  23.146 +         THEN (resolve_tac ctxt @{thms rp_inv_image_rp} 1)
  23.147 +         THEN (resolve_tac ctxt [order_rpair ms_rp label] 1)
  23.148           THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
  23.149           THEN unfold_tac ctxt @{thms rp_inv_image_def}
  23.150           THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
  23.151 @@ -300,7 +300,7 @@
  23.152        NONE => no_tac
  23.153      | SOME cert =>
  23.154          SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
  23.155 -        THEN TRY (rtac @{thm wf_empty} i))
  23.156 +        THEN TRY (resolve_tac ctxt @{thms wf_empty} i))
  23.157    end)
  23.158  
  23.159  fun gen_decomp_scnp_tac orders autom_tac ctxt =
  23.160 @@ -315,7 +315,7 @@
  23.161  fun gen_sizechange_tac orders autom_tac ctxt =
  23.162    TRY (Function_Common.termination_rule_tac ctxt 1)
  23.163    THEN TRY (Termination.wf_union_tac ctxt)
  23.164 -  THEN (rtac @{thm wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
  23.165 +  THEN (resolve_tac ctxt @{thms wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
  23.166  
  23.167  fun sizechange_tac ctxt autom_tac =
  23.168    gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
    24.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Jul 18 20:37:16 2015 +0200
    24.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Jul 18 20:47:08 2015 +0200
    24.3 @@ -289,13 +289,13 @@
    24.4          |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
    24.5  
    24.6      fun solve_membership_tac i =
    24.7 -      (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
    24.8 -      THEN' (fn j => TRY (rtac @{thm UnI1} j))
    24.9 -      THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
   24.10 -      THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
   24.11 -      THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
   24.12 -        ORELSE' ((rtac @{thm conjI})
   24.13 -          THEN' (rtac @{thm refl})
   24.14 +      (EVERY' (replicate (i - 2) (resolve_tac ctxt @{thms UnI2}))  (* pick the right component of the union *)
   24.15 +      THEN' (fn j => TRY (resolve_tac ctxt @{thms UnI1} j))
   24.16 +      THEN' (resolve_tac ctxt @{thms CollectI})                    (* unfold comprehension *)
   24.17 +      THEN' (fn i => REPEAT (resolve_tac ctxt @{thms exI} i))      (* Turn existentials into schematic Vars *)
   24.18 +      THEN' ((resolve_tac ctxt @{thms refl})                       (* unification instantiates all Vars *)
   24.19 +        ORELSE' ((resolve_tac ctxt @{thms conjI})
   24.20 +          THEN' (resolve_tac ctxt @{thms refl})
   24.21            THEN' (blast_tac ctxt)))    (* Solve rest of context... not very elegant *)
   24.22        ) i
   24.23    in
   24.24 @@ -318,10 +318,10 @@
   24.25       then Term_Graph.add_edge (c2, c1) else I)
   24.26       cs cs
   24.27  
   24.28 -fun ucomp_empty_tac T =
   24.29 -  REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
   24.30 -    ORELSE' rtac @{thm union_comp_emptyL}
   24.31 -    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
   24.32 +fun ucomp_empty_tac ctxt T =
   24.33 +  REPEAT_ALL_NEW (resolve_tac ctxt @{thms union_comp_emptyR}
   24.34 +    ORELSE' resolve_tac ctxt @{thms union_comp_emptyL}
   24.35 +    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => resolve_tac ctxt [T c1 c2] i))
   24.36  
   24.37  fun regroup_calls_tac ctxt cs = CALLS (fn (cs', i) =>
   24.38   let
   24.39 @@ -332,11 +332,13 @@
   24.40   end)
   24.41  
   24.42  
   24.43 -fun solve_trivial_tac D = CALLS (fn ([c], i) =>
   24.44 -  (case get_chain D c c of
   24.45 -     SOME (SOME thm) => rtac @{thm wf_no_loop} i
   24.46 -                        THEN rtac thm i
   24.47 -   | _ => no_tac)
   24.48 +fun solve_trivial_tac ctxt D =
   24.49 +  CALLS (fn ([c], i) =>
   24.50 +    (case get_chain D c c of
   24.51 +      SOME (SOME thm) =>
   24.52 +        resolve_tac ctxt @{thms wf_no_loop} i THEN
   24.53 +        resolve_tac ctxt [thm] i
   24.54 +    | _ => no_tac)
   24.55    | _ => no_tac)
   24.56  
   24.57  fun decompose_tac ctxt D = CALLS (fn (cs, i) =>
   24.58 @@ -344,17 +346,17 @@
   24.59      val G = mk_dgraph D cs
   24.60      val sccs = Term_Graph.strong_conn G
   24.61  
   24.62 -    fun split [SCC] i = TRY (solve_trivial_tac D i)
   24.63 +    fun split [SCC] i = TRY (solve_trivial_tac ctxt D i)
   24.64        | split (SCC::rest) i =
   24.65          regroup_calls_tac ctxt SCC i
   24.66 -        THEN rtac @{thm wf_union_compatible} i
   24.67 -        THEN rtac @{thm less_by_empty} (i + 2)
   24.68 -        THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
   24.69 +        THEN resolve_tac ctxt @{thms wf_union_compatible} i
   24.70 +        THEN resolve_tac ctxt @{thms less_by_empty} (i + 2)
   24.71 +        THEN ucomp_empty_tac ctxt (the o the oo get_chain D) (i + 2)
   24.72          THEN split rest (i + 1)
   24.73 -        THEN TRY (solve_trivial_tac D i)
   24.74 +        THEN TRY (solve_trivial_tac ctxt D i)
   24.75    in
   24.76      if length sccs > 1 then split sccs i
   24.77 -    else solve_trivial_tac D i
   24.78 +    else solve_trivial_tac ctxt D i
   24.79    end)
   24.80  
   24.81  end
    25.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat Jul 18 20:37:16 2015 +0200
    25.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat Jul 18 20:47:08 2015 +0200
    25.3 @@ -413,7 +413,7 @@
    25.4           case_tac exhaust_rule ctxt THEN_ALL_NEW (
    25.5          EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
    25.6          Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 
    25.7 -        REPEAT_DETERM o etac ctxt conjE, atac])) i
    25.8 +        REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])) i
    25.9      val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps
   25.10      val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
   25.11      val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualified true
   25.12 @@ -560,7 +560,7 @@
   25.13  
   25.14          fun non_empty_typedef_tac non_empty_pred ctxt i =
   25.15            (Method.insert_tac [non_empty_pred] THEN' 
   25.16 -            SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' atac) i
   25.17 +            SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
   25.18          val uTname = unique_Tname (rty, qty)
   25.19          val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
   25.20          val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
    26.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Jul 18 20:37:16 2015 +0200
    26.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Jul 18 20:47:08 2015 +0200
    26.3 @@ -188,7 +188,9 @@
    26.4          (fn (((name, mx), tvs), c) =>
    26.5            Typedef.add_typedef_global false (name, tvs, mx)
    26.6              (Collect $ Const (c, UnivT')) NONE
    26.7 -            (fn ctxt => rtac exI 1 THEN rtac CollectI 1 THEN
    26.8 +            (fn ctxt =>
    26.9 +              resolve_tac ctxt [exI] 1 THEN
   26.10 +              resolve_tac ctxt [CollectI] 1 THEN
   26.11                QUIET_BREADTH_FIRST (has_fewer_prems 1)
   26.12                (resolve_tac ctxt rep_intrs 1)))
   26.13          (types_syntax ~~ tyvars ~~ take (length newTs) rep_set_names)
   26.14 @@ -355,7 +357,8 @@
   26.15          val rewrites = def_thms @ map mk_meta_eq rec_rewrites;
   26.16          val char_thms' =
   26.17            map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn
   26.18 -            (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac refl 1])) eqns;
   26.19 +            (fn {context = ctxt, ...} =>
   26.20 +              EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt [refl] 1])) eqns;
   26.21  
   26.22        in (thy', char_thms' @ char_thms) end;
   26.23  
   26.24 @@ -382,8 +385,11 @@
   26.25                     (map (pair "x") Ts, S $ Old_Datatype_Aux.app_bnds f i)),
   26.26                   HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
   26.27                     (r $ (a $ Old_Datatype_Aux.app_bnds f i)), f))))
   26.28 -              (fn {context = ctxt, ...} => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
   26.29 -                 REPEAT (etac allE 1), rtac thm 1, assume_tac ctxt 1])
   26.30 +              (fn {context = ctxt, ...} =>
   26.31 +                EVERY [REPEAT_DETERM_N i (resolve_tac ctxt @{thms ext} 1),
   26.32 +                 REPEAT (eresolve_tac ctxt [allE] 1),
   26.33 +                 resolve_tac ctxt [thm] 1,
   26.34 +                 assume_tac ctxt 1])
   26.35            end
   26.36        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   26.37  
   26.38 @@ -421,7 +427,7 @@
   26.39                [(Old_Datatype_Aux.ind_tac ctxt induct [] THEN_ALL_NEW
   26.40                    Object_Logic.atomize_prems_tac ctxt) 1,
   26.41                 REPEAT (EVERY
   26.42 -                 [rtac allI 1, rtac impI 1,
   26.43 +                 [resolve_tac ctxt [allI] 1, resolve_tac ctxt [impI] 1,
   26.44                    Old_Datatype_Aux.exh_tac ctxt (exh_thm_of dt_info) 1,
   26.45                    REPEAT (EVERY
   26.46                      [hyp_subst_tac ctxt 1,
   26.47 @@ -431,9 +437,9 @@
   26.48                       ORELSE (EVERY
   26.49                         [REPEAT (eresolve_tac ctxt (Scons_inject ::
   26.50                            map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
   26.51 -                        REPEAT (cong_tac ctxt 1), rtac refl 1,
   26.52 +                        REPEAT (cong_tac ctxt 1), resolve_tac ctxt [refl] 1,
   26.53                          REPEAT (assume_tac ctxt 1 ORELSE (EVERY
   26.54 -                          [REPEAT (rtac @{thm ext} 1),
   26.55 +                          [REPEAT (resolve_tac ctxt @{thms ext} 1),
   26.56                             REPEAT (eresolve_tac ctxt (mp :: allE ::
   26.57                               map make_elim (Suml_inject :: Sumr_inject ::
   26.58                                 Lim_inject :: inj_thms') @ fun_congs) 1),
   26.59 @@ -450,7 +456,7 @@
   26.60                    Object_Logic.atomize_prems_tac ctxt) 1,
   26.61                  rewrite_goals_tac ctxt rewrites,
   26.62                  REPEAT ((resolve_tac ctxt rep_intrs THEN_ALL_NEW
   26.63 -                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
   26.64 +                  ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac elem_thms)) 1)]);
   26.65  
   26.66        in (inj_thms'' @ inj_thms, elem_thms @ Old_Datatype_Aux.split_conj_thm elem_thm) end;
   26.67  
   26.68 @@ -485,7 +491,7 @@
   26.69            (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
   26.70               [(Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
   26.71                   Object_Logic.atomize_prems_tac ctxt) 1,
   26.72 -              REPEAT (rtac TrueI 1),
   26.73 +              REPEAT (resolve_tac ctxt [TrueI] 1),
   26.74                rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} ::
   26.75                  Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
   26.76                rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
   26.77 @@ -493,7 +499,7 @@
   26.78                  [REPEAT (eresolve_tac ctxt ([rangeE, @{thm ex1_implies_ex} RS exE] @
   26.79                     maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
   26.80                   TRY (hyp_subst_tac ctxt 1),
   26.81 -                 rtac (sym RS range_eqI) 1,
   26.82 +                 resolve_tac ctxt [sym RS range_eqI] 1,
   26.83                   resolve_tac ctxt iso_char_thms 1])])));
   26.84  
   26.85      val Abs_inverse_thms' =
   26.86 @@ -518,7 +524,7 @@
   26.87          (fn {context = ctxt, ...} => EVERY
   26.88            [resolve_tac ctxt inj_thms 1,
   26.89             rewrite_goals_tac ctxt rewrites,
   26.90 -           rtac refl 3,
   26.91 +           resolve_tac ctxt [refl] 3,
   26.92             resolve_tac ctxt rep_intrs 2,
   26.93             REPEAT (resolve_tac ctxt iso_elem_thms 1)])
   26.94        end;
   26.95 @@ -560,12 +566,14 @@
   26.96        in
   26.97          Goal.prove_sorry_global thy5 [] [] t
   26.98            (fn {context = ctxt, ...} => EVERY
   26.99 -            [rtac iffI 1,
  26.100 -             REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
  26.101 -             dresolve_tac ctxt rep_congs 1, dtac @{thm box_equals} 1,
  26.102 +            [resolve_tac ctxt [iffI] 1,
  26.103 +             REPEAT (eresolve_tac ctxt [conjE] 2), hyp_subst_tac ctxt 2,
  26.104 +             resolve_tac ctxt [refl] 2,
  26.105 +             dresolve_tac ctxt rep_congs 1,
  26.106 +             dresolve_tac ctxt @{thms box_equals} 1,
  26.107               REPEAT (resolve_tac ctxt rep_thms 1),
  26.108               REPEAT (eresolve_tac ctxt inj_thms 1),
  26.109 -             REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1),
  26.110 +             REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (resolve_tac ctxt @{thms ext} 1),
  26.111                 REPEAT (eresolve_tac ctxt (make_elim fun_cong :: inj_thms) 1),
  26.112                 assume_tac ctxt 1]))])
  26.113        end;
  26.114 @@ -618,10 +626,10 @@
  26.115             HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_concls)))
  26.116          (fn {context = ctxt, ...} =>
  26.117            EVERY
  26.118 -           [REPEAT (etac conjE 1),
  26.119 +           [REPEAT (eresolve_tac ctxt [conjE] 1),
  26.120              REPEAT (EVERY
  26.121 -              [TRY (rtac conjI 1), resolve_tac ctxt Rep_inverse_thms 1,
  26.122 -               etac mp 1, resolve_tac ctxt iso_elem_thms 1])]);
  26.123 +              [TRY (resolve_tac ctxt [conjI] 1), resolve_tac ctxt Rep_inverse_thms 1,
  26.124 +               eresolve_tac ctxt [mp] 1, resolve_tac ctxt iso_elem_thms 1])]);
  26.125  
  26.126      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma)));
  26.127      val frees =
  26.128 @@ -637,14 +645,14 @@
  26.129        (Logic.strip_imp_concl dt_induct_prop)
  26.130        (fn {context = ctxt, prems, ...} =>
  26.131          EVERY
  26.132 -          [rtac indrule_lemma' 1,
  26.133 +          [resolve_tac ctxt [indrule_lemma'] 1,
  26.134             (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
  26.135                Object_Logic.atomize_prems_tac ctxt) 1,
  26.136             EVERY (map (fn (prem, r) => (EVERY
  26.137               [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
  26.138                simp_tac (put_simpset HOL_basic_ss ctxt
  26.139                  addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
  26.140 -              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
  26.141 +              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
  26.142                    (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
  26.143  
  26.144      val ([(_, [dt_induct'])], thy7) =
    27.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jul 18 20:37:16 2015 +0200
    27.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jul 18 20:47:08 2015 +0200
    27.3 @@ -249,7 +249,7 @@
    27.4          val thesis =
    27.5            Thm.instantiate ([], inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2))
    27.6              case_th' OF prems2
    27.7 -      in rtac thesis 1 end
    27.8 +      in resolve_tac ctxt2 [thesis] 1 end
    27.9    in
   27.10      Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule
   27.11        (fn {context = ctxt1, ...} =>
    28.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jul 18 20:37:16 2015 +0200
    28.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jul 18 20:47:08 2015 +0200
    28.3 @@ -1106,7 +1106,7 @@
    28.4            val tac =
    28.5              Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
    28.6                (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
    28.7 -            THEN rtac @{thm Predicate.singleI} 1
    28.8 +            THEN resolve_tac ctxt @{thms Predicate.singleI} 1
    28.9          in SOME (Goal.prove ctxt (argnames @ hoarg_names') []
   28.10              neg_introtrm (fn _ => tac))
   28.11          end
    29.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Jul 18 20:37:16 2015 +0200
    29.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Jul 18 20:47:08 2015 +0200
    29.3 @@ -166,8 +166,9 @@
    29.4              val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
    29.5                THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
    29.6                THEN (EVERY (map (fn y =>
    29.7 -                rtac (Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}) 1) ps))
    29.8 -              THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
    29.9 +                resolve_tac ctxt'
   29.10 +                  [Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
   29.11 +              THEN REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 THEN assume_tac ctxt' 1)
   29.12                THEN TRY (assume_tac ctxt' 1)
   29.13            in
   29.14              Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac)
    30.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Jul 18 20:37:16 2015 +0200
    30.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Jul 18 20:47:08 2015 +0200
    30.3 @@ -38,7 +38,7 @@
    30.4    simpset_of (put_simpset HOL_basic_ss @{context}
    30.5      addsimps @{thms simp_thms Pair_eq}
    30.6      setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
    30.7 -    setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI})))
    30.8 +    setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
    30.9  
   30.10  
   30.11  (* auxillary functions *)
   30.12 @@ -74,13 +74,13 @@
   30.13            end) ctxt 1
   30.14        | Abs _ => raise Fail "prove_param: No valid parameter term")
   30.15    in
   30.16 -    REPEAT_DETERM (rtac @{thm ext} 1)
   30.17 +    REPEAT_DETERM (resolve_tac ctxt @{thms ext} 1)
   30.18      THEN trace_tac ctxt options "prove_param"
   30.19      THEN f_tac
   30.20      THEN trace_tac ctxt options "after prove_param"
   30.21      THEN (REPEAT_DETERM (assume_tac ctxt 1))
   30.22      THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   30.23 -    THEN REPEAT_DETERM (rtac @{thm refl} 1)
   30.24 +    THEN REPEAT_DETERM (resolve_tac ctxt @{thms refl} 1)
   30.25    end
   30.26  
   30.27  fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
   30.28 @@ -93,7 +93,7 @@
   30.29          val ho_args = ho_args_of mode args
   30.30        in
   30.31          trace_tac ctxt options "before intro rule:"
   30.32 -        THEN rtac introrule 1
   30.33 +        THEN resolve_tac ctxt [introrule] 1
   30.34          THEN trace_tac ctxt options "after intro rule"
   30.35          (* for the right assumption in first position *)
   30.36          THEN rotate_tac premposition 1
   30.37 @@ -118,7 +118,7 @@
   30.38                  [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
   30.39                param_prem
   30.40            in
   30.41 -            rtac param_prem' 1
   30.42 +            resolve_tac ctxt' [param_prem'] 1
   30.43            end) ctxt 1
   30.44        THEN trace_tac ctxt options "after prove parameter call")
   30.45  
   30.46 @@ -144,9 +144,9 @@
   30.47      asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
   30.48      THEN trace_tac ctxt options "after prove_match:"
   30.49      THEN (DETERM (TRY
   30.50 -           (rtac eval_if_P 1
   30.51 +           (resolve_tac ctxt [eval_if_P] 1
   30.52             THEN (SUBPROOF (fn {prems, context = ctxt', ...} =>
   30.53 -             (REPEAT_DETERM (rtac @{thm conjI} 1
   30.54 +             (REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1
   30.55               THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1))))
   30.56               THEN trace_tac ctxt' options "if condition to be solved:"
   30.57               THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1
   30.58 @@ -157,7 +157,7 @@
   30.59                    rewrite_goal_tac ctxt'
   30.60                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   30.61                  end
   30.62 -             THEN REPEAT_DETERM (rtac @{thm refl} 1))
   30.63 +             THEN REPEAT_DETERM (resolve_tac ctxt' @{thms refl} 1))
   30.64               THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1))))
   30.65      THEN trace_tac ctxt options "after if simplification"
   30.66    end;
   30.67 @@ -199,13 +199,13 @@
   30.68              in
   30.69                rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   30.70              end) ctxt 1
   30.71 -        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
   30.72 +        THEN (resolve_tac ctxt [if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}] 1)
   30.73      | prove_prems out_ts ((p, deriv) :: ps) =
   30.74          let
   30.75            val premposition = (find_index (equal p) clauses) + nargs
   30.76            val mode = head_mode_of deriv
   30.77            val rest_tac =
   30.78 -            rtac @{thm bindI} 1
   30.79 +            resolve_tac ctxt @{thms bindI} 1
   30.80              THEN (case p of Prem t =>
   30.81                let
   30.82                  val (_, us) = strip_comb t
   30.83 @@ -238,15 +238,15 @@
   30.84                  THEN (if (is_some name) then
   30.85                      trace_tac ctxt options "before applying not introduction rule"
   30.86                      THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
   30.87 -                      rtac (the neg_intro_rule) 1
   30.88 -                      THEN rtac (nth prems premposition) 1) ctxt 1
   30.89 +                      resolve_tac ctxt [the neg_intro_rule] 1
   30.90 +                      THEN resolve_tac ctxt [nth prems premposition] 1) ctxt 1
   30.91                      THEN trace_tac ctxt options "after applying not introduction rule"
   30.92                      THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
   30.93                      THEN (REPEAT_DETERM (assume_tac ctxt 1))
   30.94                    else
   30.95 -                    rtac @{thm not_predI'} 1
   30.96 +                    resolve_tac ctxt @{thms not_predI'} 1
   30.97                      (* test: *)
   30.98 -                    THEN dtac @{thm sym} 1
   30.99 +                    THEN dresolve_tac ctxt @{thms sym} 1
  30.100                      THEN asm_full_simp_tac
  30.101                        (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
  30.102                      THEN simp_tac
  30.103 @@ -254,7 +254,7 @@
  30.104                  THEN rec_tac
  30.105                end
  30.106              | Sidecond t =>
  30.107 -             rtac @{thm if_predI} 1
  30.108 +             resolve_tac ctxt @{thms if_predI} 1
  30.109               THEN trace_tac ctxt options "before sidecond:"
  30.110               THEN prove_sidecond ctxt t
  30.111               THEN trace_tac ctxt options "after sidecond:"
  30.112 @@ -265,14 +265,14 @@
  30.113      val prems_tac = prove_prems in_ts moded_ps
  30.114    in
  30.115      trace_tac ctxt options "Proving clause..."
  30.116 -    THEN rtac @{thm bindI} 1
  30.117 -    THEN rtac @{thm singleI} 1
  30.118 +    THEN resolve_tac ctxt @{thms bindI} 1
  30.119 +    THEN resolve_tac ctxt @{thms singleI} 1
  30.120      THEN prems_tac
  30.121    end
  30.122  
  30.123 -fun select_sup 1 1 = []
  30.124 -  | select_sup _ 1 = [rtac @{thm supI1}]
  30.125 -  | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
  30.126 +fun select_sup _ 1 1 = []
  30.127 +  | select_sup ctxt _ 1 = [resolve_tac ctxt @{thms supI1}]
  30.128 +  | select_sup ctxt n i = resolve_tac ctxt @{thms supI2} :: select_sup ctxt (n - 1) (i - 1);
  30.129  
  30.130  fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
  30.131    let
  30.132 @@ -282,11 +282,11 @@
  30.133    in
  30.134      REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
  30.135      THEN trace_tac ctxt options "before applying elim rule"
  30.136 -    THEN etac (predfun_elim_of ctxt pred mode) 1
  30.137 -    THEN etac pred_case_rule 1
  30.138 +    THEN eresolve_tac ctxt [predfun_elim_of ctxt pred mode] 1
  30.139 +    THEN eresolve_tac ctxt [pred_case_rule] 1
  30.140      THEN trace_tac ctxt options "after applying elim rule"
  30.141      THEN (EVERY (map
  30.142 -           (fn i => EVERY' (select_sup (length moded_clauses) i) i)
  30.143 +           (fn i => EVERY' (select_sup ctxt (length moded_clauses) i) i)
  30.144               (1 upto (length moded_clauses))))
  30.145      THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
  30.146      THEN trace_tac ctxt options "proved one direction"
  30.147 @@ -313,15 +313,15 @@
  30.148              (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
  30.149                THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
  30.150                THEN (REPEAT_DETERM_N (num_of_constrs - 1)
  30.151 -                (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
  30.152 +                (eresolve_tac ctxt @{thms botE} 1 ORELSE eresolve_tac ctxt @{thms botE} 2)))
  30.153              THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
  30.154              THEN (EVERY (map split_term_tac ts))
  30.155            end
  30.156        else all_tac
  30.157    in
  30.158      split_term_tac (HOLogic.mk_tuple out_ts)
  30.159 -    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
  30.160 -    THEN (etac @{thm botE} 2))))
  30.161 +    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt @{thms split_if_asm} 1)
  30.162 +    THEN (eresolve_tac ctxt @{thms botE} 2))))
  30.163    end
  30.164  
  30.165  (* VERY LARGE SIMILIRATIY to function prove_param
  30.166 @@ -357,15 +357,15 @@
  30.167            val param_derivations = param_derivations_of deriv
  30.168            val ho_args = ho_args_of mode args
  30.169          in
  30.170 -          etac @{thm bindE} 1
  30.171 +          eresolve_tac ctxt @{thms bindE} 1
  30.172            THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
  30.173            THEN trace_tac ctxt options "prove_expr2-before"
  30.174 -          THEN etac (predfun_elim_of ctxt name mode) 1
  30.175 +          THEN eresolve_tac ctxt [predfun_elim_of ctxt name mode] 1
  30.176            THEN trace_tac ctxt options "prove_expr2"
  30.177            THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
  30.178            THEN trace_tac ctxt options "finished prove_expr2"
  30.179          end
  30.180 -      | _ => etac @{thm bindE} 1)
  30.181 +      | _ => eresolve_tac ctxt @{thms bindE} 1)
  30.182  
  30.183  fun prove_sidecond2 options ctxt t =
  30.184    let
  30.185 @@ -399,15 +399,15 @@
  30.186        trace_tac ctxt options "before prove_match2 - last call:"
  30.187        THEN prove_match2 options ctxt out_ts
  30.188        THEN trace_tac ctxt options "after prove_match2 - last call:"
  30.189 -      THEN (etac @{thm singleE} 1)
  30.190 -      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
  30.191 +      THEN (eresolve_tac ctxt @{thms singleE} 1)
  30.192 +      THEN (REPEAT_DETERM (eresolve_tac ctxt @{thms Pair_inject} 1))
  30.193        THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
  30.194        THEN TRY (
  30.195 -        (REPEAT_DETERM (etac @{thm Pair_inject} 1))
  30.196 +        (REPEAT_DETERM (eresolve_tac ctxt @{thms Pair_inject} 1))
  30.197          THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
  30.198  
  30.199          THEN SOLVED (trace_tac ctxt options "state before applying intro rule:"
  30.200 -        THEN (rtac pred_intro_rule
  30.201 +        THEN (resolve_tac ctxt [pred_intro_rule]
  30.202          (* How to handle equality correctly? *)
  30.203          THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
  30.204          THEN' (assume_tac ctxt ORELSE'
  30.205 @@ -438,20 +438,20 @@
  30.206                  val ho_args = ho_args_of mode args
  30.207                in
  30.208                  trace_tac ctxt options "before neg prem 2"
  30.209 -                THEN etac @{thm bindE} 1
  30.210 +                THEN eresolve_tac ctxt @{thms bindE} 1
  30.211                  THEN (if is_some name then
  30.212                      full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
  30.213                        [predfun_definition_of ctxt (the name) mode]) 1
  30.214 -                    THEN etac @{thm not_predE} 1
  30.215 +                    THEN eresolve_tac ctxt @{thms not_predE} 1
  30.216                      THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
  30.217                      THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
  30.218                    else
  30.219 -                    etac @{thm not_predE'} 1)
  30.220 +                    eresolve_tac ctxt @{thms not_predE'} 1)
  30.221                  THEN rec_tac
  30.222                end
  30.223            | Sidecond t =>
  30.224 -              etac @{thm bindE} 1
  30.225 -              THEN etac @{thm if_predE} 1
  30.226 +              eresolve_tac ctxt @{thms bindE} 1
  30.227 +              THEN eresolve_tac ctxt @{thms if_predE} 1
  30.228                THEN prove_sidecond2 options ctxt t
  30.229                THEN prove_prems2 [] ps)
  30.230        in
  30.231 @@ -463,9 +463,9 @@
  30.232      val prems_tac = prove_prems2 in_ts ps
  30.233    in
  30.234      trace_tac ctxt options "starting prove_clause2"
  30.235 -    THEN etac @{thm bindE} 1
  30.236 -    THEN (etac @{thm singleE'} 1)
  30.237 -    THEN (TRY (etac @{thm Pair_inject} 1))
  30.238 +    THEN eresolve_tac ctxt @{thms bindE} 1
  30.239 +    THEN (eresolve_tac ctxt @{thms singleE'} 1)
  30.240 +    THEN (TRY (eresolve_tac ctxt @{thms Pair_inject} 1))
  30.241      THEN trace_tac ctxt options "after singleE':"
  30.242      THEN prems_tac
  30.243    end;
  30.244 @@ -473,15 +473,15 @@
  30.245  fun prove_other_direction options ctxt pred mode moded_clauses =
  30.246    let
  30.247      fun prove_clause clause i =
  30.248 -      (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
  30.249 +      (if i < length moded_clauses then eresolve_tac ctxt @{thms supE} 1 else all_tac)
  30.250        THEN (prove_clause2 options ctxt pred mode clause i)
  30.251    in
  30.252 -    (DETERM (TRY (rtac @{thm unit.induct} 1)))
  30.253 +    (DETERM (TRY (resolve_tac ctxt @{thms unit.induct} 1)))
  30.254       THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
  30.255 -     THEN (rtac (predfun_intro_of ctxt pred mode) 1)
  30.256 -     THEN (REPEAT_DETERM (rtac @{thm refl} 2))
  30.257 +     THEN (resolve_tac ctxt [predfun_intro_of ctxt pred mode] 1)
  30.258 +     THEN (REPEAT_DETERM (resolve_tac ctxt @{thms refl} 2))
  30.259       THEN (
  30.260 -       if null moded_clauses then etac @{thm botE} 1
  30.261 +       if null moded_clauses then eresolve_tac ctxt @{thms botE} 1
  30.262         else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
  30.263    end
  30.264  
  30.265 @@ -496,7 +496,7 @@
  30.266      Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
  30.267        (if not (skip_proof options) then
  30.268          (fn _ =>
  30.269 -        rtac @{thm pred_iffI} 1
  30.270 +        resolve_tac ctxt @{thms pred_iffI} 1
  30.271          THEN trace_tac ctxt options "after pred_iffI"
  30.272          THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
  30.273          THEN trace_tac ctxt options "proved one direction"
    31.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Jul 18 20:37:16 2015 +0200
    31.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Jul 18 20:47:08 2015 +0200
    31.3 @@ -741,7 +741,7 @@
    31.4          (case try (fn () =>
    31.5              Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
    31.6            NONE => no_tac
    31.7 -        | SOME r => rtac r i)
    31.8 +        | SOME r => resolve_tac ctxt [r] i)
    31.9      end)
   31.10  end;
   31.11  
   31.12 @@ -860,11 +860,11 @@
   31.13         else Conv.arg_conv (conv ctxt) p
   31.14       val p' = Thm.rhs_of cpth
   31.15       val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
   31.16 -   in rtac th i end
   31.17 +   in resolve_tac ctxt [th] i end
   31.18     handle COOPER _ => no_tac);
   31.19  
   31.20 -fun finish_tac q = SUBGOAL (fn (_, i) =>
   31.21 -  (if q then I else TRY) (rtac TrueI i));
   31.22 +fun finish_tac ctxt q = SUBGOAL (fn (_, i) =>
   31.23 +  (if q then I else TRY) (resolve_tac ctxt [TrueI] i));
   31.24  
   31.25  fun tac elim add_ths del_ths = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} =>
   31.26    let
   31.27 @@ -885,7 +885,7 @@
   31.28      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   31.29      THEN_ALL_NEW nat_to_int_tac ctxt
   31.30      THEN_ALL_NEW core_tac ctxt
   31.31 -    THEN_ALL_NEW finish_tac elim
   31.32 +    THEN_ALL_NEW finish_tac ctxt elim
   31.33    end 1);
   31.34  
   31.35  
    32.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Jul 18 20:37:16 2015 +0200
    32.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Jul 18 20:47:08 2015 +0200
    32.3 @@ -108,7 +108,7 @@
    32.4            [(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
    32.5             (cT_rhs, Thm.cterm_of lthy' t_rhs)]);
    32.6      fun tac ctxt =
    32.7 -      ALLGOALS (rtac rule)
    32.8 +      ALLGOALS (resolve_tac ctxt [rule])
    32.9        THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
   32.10        THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2));
   32.11      val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
    33.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Jul 18 20:37:16 2015 +0200
    33.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Jul 18 20:47:08 2015 +0200
    33.3 @@ -9,15 +9,12 @@
    33.4    val add_quotient_def:
    33.5      ((binding * mixfix) * Attrib.binding) * (term * term) -> thm ->
    33.6      local_theory -> Quotient_Info.quotconsts * local_theory
    33.7 -
    33.8    val quotient_def:
    33.9      (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
   33.10      local_theory -> Proof.state
   33.11 -
   33.12    val quotient_def_cmd:
   33.13      (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
   33.14      local_theory -> Proof.state
   33.15 -
   33.16  end;
   33.17  
   33.18  structure Quotient_Def: QUOTIENT_DEF =
   33.19 @@ -189,7 +186,9 @@
   33.20            case thm_list of
   33.21              [] => the maybe_proven_rsp_thm
   33.22            | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
   33.23 -            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
   33.24 +            (fn _ =>
   33.25 +              resolve_tac ctxt [readable_rsp_thm_eq] 1 THEN
   33.26 +              Proof_Context.fact_tac ctxt [thm] 1)
   33.27        in
   33.28          snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
   33.29        end
    34.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Jul 18 20:37:16 2015 +0200
    34.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Jul 18 20:47:08 2015 +0200
    34.3 @@ -61,7 +61,7 @@
    34.4  
    34.5  fun quotient_tac ctxt =
    34.6    (REPEAT_ALL_NEW (FIRST'
    34.7 -    [rtac @{thm identity_quotient3},
    34.8 +    [resolve_tac ctxt @{thms identity_quotient3},
    34.9       resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_thm}))]))
   34.10  
   34.11  val quotient_solver = mk_solver "Quotient goal solver" quotient_tac
   34.12 @@ -250,7 +250,7 @@
   34.13                val inst_thm = Drule.instantiate' ty_inst
   34.14                  ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
   34.15              in
   34.16 -              (rtac inst_thm THEN' SOLVED' (quotient_tac ctxt)) 1
   34.17 +              (resolve_tac ctxt [inst_thm] THEN' SOLVED' (quotient_tac ctxt)) 1
   34.18              end
   34.19        | _ => no_tac
   34.20      end)
   34.21 @@ -266,7 +266,7 @@
   34.22        in
   34.23          case try (Drule.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
   34.24              [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
   34.25 -          SOME thm => rtac thm THEN' quotient_tac ctxt
   34.26 +          SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
   34.27          | NONE => K no_tac
   34.28        end
   34.29    | _ => K no_tac
   34.30 @@ -282,7 +282,7 @@
   34.31            case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of
   34.32              SOME t_inst =>
   34.33                (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
   34.34 -                SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
   34.35 +                SOME inst_thm => (resolve_tac ctxt [inst_thm] THEN' quotient_tac ctxt) i
   34.36                | NONE => no_tac)
   34.37            | NONE => no_tac
   34.38          end
   34.39 @@ -315,48 +315,48 @@
   34.40    (case bare_concl goal of
   34.41        (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
   34.42      (Const (@{const_name rel_fun}, _) $ _ $ _) $ (Abs _) $ (Abs _)
   34.43 -        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
   34.44 +        => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
   34.45  
   34.46        (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
   34.47    | (Const (@{const_name HOL.eq},_) $
   34.48        (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   34.49        (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   34.50 -        => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
   34.51 +        => resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
   34.52  
   34.53        (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
   34.54    | (Const (@{const_name rel_fun}, _) $ _ $ _) $
   34.55        (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   34.56        (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   34.57 -        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
   34.58 +        => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
   34.59  
   34.60        (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   34.61    | Const (@{const_name HOL.eq},_) $
   34.62        (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   34.63        (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   34.64 -        => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
   34.65 +        => resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
   34.66  
   34.67        (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
   34.68    | (Const (@{const_name rel_fun}, _) $ _ $ _) $
   34.69        (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   34.70        (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   34.71 -        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
   34.72 +        => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
   34.73  
   34.74    | (Const (@{const_name rel_fun}, _) $ _ $ _) $
   34.75        (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
   34.76 -        => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
   34.77 +        => resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
   34.78  
   34.79    | (_ $
   34.80        (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   34.81        (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   34.82 -        => rtac @{thm babs_rsp} THEN' quotient_tac ctxt
   34.83 +        => resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
   34.84  
   34.85    | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
   34.86 -     (rtac @{thm refl} ORELSE'
   34.87 +     (resolve_tac ctxt @{thms refl} ORELSE'
   34.88        (equals_rsp_tac R ctxt THEN' RANGE [
   34.89           quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
   34.90  
   34.91        (* reflexivity of operators arising from Cong_tac *)
   34.92 -  | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
   34.93 +  | Const (@{const_name HOL.eq},_) $ _ $ _ => resolve_tac ctxt @{thms refl}
   34.94  
   34.95       (* respectfulness of constants; in particular of a simple relation *)
   34.96    | _ $ (Const _) $ (Const _)  (* rel_fun, list_rel, etc but not equality *)
   34.97 @@ -366,7 +366,7 @@
   34.98        (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
   34.99        (* observe map_fun *)
  34.100    | _ $ _ $ _
  34.101 -      => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
  34.102 +      => (resolve_tac ctxt @{thms quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
  34.103           ORELSE' rep_abs_rsp_tac ctxt
  34.104  
  34.105    | _ => K no_tac) i)
  34.106 @@ -388,7 +388,7 @@
  34.107      assume_tac ctxt,
  34.108  
  34.109      (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
  34.110 -    rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
  34.111 +    resolve_tac ctxt @{thms ext} THEN' quot_true_tac ctxt unlam,
  34.112  
  34.113      (* reflexivity of the basic relations *)
  34.114      (* R ... ... *)
  34.115 @@ -522,7 +522,7 @@
  34.116        map_fun_tac ctxt,
  34.117        lambda_prs_tac ctxt,
  34.118        simp_tac simpset,
  34.119 -      TRY o rtac refl]
  34.120 +      TRY o resolve_tac ctxt [refl]]
  34.121    end
  34.122  
  34.123  
  34.124 @@ -531,8 +531,8 @@
  34.125  fun inst_spec ctrm =
  34.126    Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
  34.127  
  34.128 -fun inst_spec_tac ctrms =
  34.129 -  EVERY' (map (dtac o inst_spec) ctrms)
  34.130 +fun inst_spec_tac ctxt ctrms =
  34.131 +  EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)
  34.132  
  34.133  fun all_list xs trm =
  34.134    fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
  34.135 @@ -548,9 +548,9 @@
  34.136        val concl' = apply_under_Trueprop (all_list vrs) concl
  34.137        val goal = Logic.mk_implies (concl', concl)
  34.138        val rule = Goal.prove ctxt [] [] goal
  34.139 -        (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt]))
  34.140 +        (K (EVERY1 [inst_spec_tac ctxt (rev cvrs), assume_tac ctxt]))
  34.141      in
  34.142 -      rtac rule i
  34.143 +      resolve_tac ctxt [rule] i
  34.144      end)
  34.145  
  34.146  
  34.147 @@ -632,7 +632,7 @@
  34.148          val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
  34.149          val rule = procedure_inst ctxt rtrm  goal
  34.150        in
  34.151 -        rtac rule i
  34.152 +        resolve_tac ctxt [rule] i
  34.153        end)
  34.154    end
  34.155  
  34.156 @@ -681,7 +681,7 @@
  34.157          val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
  34.158          val rule = partiality_procedure_inst ctxt rtrm  goal
  34.159        in
  34.160 -        rtac rule i
  34.161 +        resolve_tac ctxt [rule] i
  34.162        end)
  34.163    end
  34.164  
  34.165 @@ -722,7 +722,7 @@
  34.166  
  34.167          val rule = procedure_inst ctxt (Thm.prop_of rthm') goal
  34.168        in
  34.169 -        (rtac rule THEN' rtac rthm') i
  34.170 +        (resolve_tac ctxt [rule] THEN' resolve_tac ctxt [rthm']) i
  34.171        end)
  34.172    end
  34.173  
    35.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Sat Jul 18 20:37:16 2015 +0200
    35.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Sat Jul 18 20:47:08 2015 +0200
    35.3 @@ -42,8 +42,8 @@
    35.4  (* makes the new type definitions and proves non-emptyness *)
    35.5  fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
    35.6    let
    35.7 -    fun typedef_tac _ =
    35.8 -      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
    35.9 +    fun typedef_tac ctxt =
   35.10 +      EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
   35.11    in
   35.12      Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx)
   35.13        (typedef_term rel rty lthy) NONE typedef_tac lthy
   35.14 @@ -58,12 +58,12 @@
   35.15      val abs_inv = #Abs_inverse typedef_info
   35.16      val rep_inj = #Rep_inject typedef_info
   35.17    in
   35.18 -    (rtac @{thm quot_type.intro} THEN' RANGE [
   35.19 -      rtac equiv_thm,
   35.20 -      rtac rep_thm,
   35.21 -      rtac rep_inv,
   35.22 -      rtac abs_inv THEN' rtac mem_def2 THEN' assume_tac ctxt,
   35.23 -      rtac rep_inj]) 1
   35.24 +    (resolve_tac ctxt @{thms quot_type.intro} THEN' RANGE [
   35.25 +      resolve_tac ctxt [equiv_thm],
   35.26 +      resolve_tac ctxt [rep_thm],
   35.27 +      resolve_tac ctxt [rep_inv],
   35.28 +      resolve_tac ctxt [abs_inv] THEN' resolve_tac ctxt [mem_def2] THEN' assume_tac ctxt,
   35.29 +      resolve_tac ctxt [rep_inj]]) 1
   35.30    end
   35.31  
   35.32  (* proves the quot_type theorem for the new type *)
    36.1 --- a/src/HOL/Tools/SMT/conj_disj_perm.ML	Sat Jul 18 20:37:16 2015 +0200
    36.2 +++ b/src/HOL/Tools/SMT/conj_disj_perm.ML	Sat Jul 18 20:47:08 2015 +0200
    36.3 @@ -6,7 +6,7 @@
    36.4  
    36.5  signature CONJ_DISJ_PERM =
    36.6  sig
    36.7 -  val conj_disj_perm_tac: int -> tactic
    36.8 +  val conj_disj_perm_tac: Proof.context -> int -> tactic
    36.9  end
   36.10  
   36.11  structure Conj_Disj_Perm: CONJ_DISJ_PERM =
   36.12 @@ -118,10 +118,10 @@
   36.13    | (True, Disj) => contrapos (prove_contradiction_eq false) cp
   36.14    | _ => raise CTERM ("prove_conj_disj_perm", [ct]))
   36.15  
   36.16 -val conj_disj_perm_tac = CSUBGOAL (fn (ct, i) => 
   36.17 +fun conj_disj_perm_tac ctxt = CSUBGOAL (fn (ct, i) => 
   36.18    (case Thm.term_of ct of
   36.19      @{const HOL.Trueprop} $ (@{const HOL.eq(bool)} $ _ $ _) =>
   36.20 -      rtac (prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))) i
   36.21 +      resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i
   36.22    | _ => no_tac))
   36.23  
   36.24  end
    37.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Sat Jul 18 20:37:16 2015 +0200
    37.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Sat Jul 18 20:47:08 2015 +0200
    37.3 @@ -289,13 +289,14 @@
    37.4            "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")
    37.5      | SMT_Failure.SMT fail => error (str_of ctxt fail)
    37.6  
    37.7 -  fun resolve (SOME thm) = rtac thm 1
    37.8 -    | resolve NONE = no_tac
    37.9 +  fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1
   37.10 +    | resolve _ NONE = no_tac
   37.11  
   37.12    fun tac prove ctxt rules =
   37.13      CONVERSION (SMT_Normalize.atomize_conv ctxt)
   37.14 -    THEN' rtac @{thm ccontr}
   37.15 -    THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve (prove ctxt' (rules @ prems))) ctxt
   37.16 +    THEN' resolve_tac ctxt @{thms ccontr}
   37.17 +    THEN' SUBPROOF (fn {context = ctxt', prems, ...} =>
   37.18 +      resolve ctxt' (prove ctxt' (rules @ prems))) ctxt
   37.19  in
   37.20  
   37.21  val smt_tac = tac safe_solve
    38.1 --- a/src/HOL/Tools/SMT/z3_replay.ML	Sat Jul 18 20:37:16 2015 +0200
    38.2 +++ b/src/HOL/Tools/SMT/z3_replay.ML	Sat Jul 18 20:47:08 2015 +0200
    38.3 @@ -148,10 +148,10 @@
    38.4  in
    38.5  
    38.6  fun discharge_sk_tac ctxt i st =
    38.7 -  (rtac @{thm trans} i
    38.8 +  (resolve_tac ctxt @{thms trans} i
    38.9     THEN resolve_tac ctxt sk_rules i
   38.10 -   THEN (rtac @{thm refl} ORELSE' discharge_sk_tac ctxt) (i+1)
   38.11 -   THEN rtac @{thm refl} i) st
   38.12 +   THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1)
   38.13 +   THEN resolve_tac ctxt @{thms refl} i) st
   38.14  
   38.15  end
   38.16  
    39.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sat Jul 18 20:37:16 2015 +0200
    39.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sat Jul 18 20:47:08 2015 +0200
    39.3 @@ -443,9 +443,9 @@
    39.4  fun lift_ite_rewrite ctxt t =
    39.5    prove ctxt t (fn ctxt => 
    39.6      CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt)))
    39.7 -    THEN' rtac @{thm refl})
    39.8 +    THEN' resolve_tac ctxt @{thms refl})
    39.9  
   39.10 -fun prove_conj_disj_perm ctxt t = prove ctxt t (fn _ => Conj_Disj_Perm.conj_disj_perm_tac)
   39.11 +fun prove_conj_disj_perm ctxt t = prove ctxt t Conj_Disj_Perm.conj_disj_perm_tac
   39.12  
   39.13  fun rewrite ctxt _ = try_provers ctxt Z3_Proof.Rewrite [
   39.14    ("rules", apply_rule ctxt),
   39.15 @@ -492,8 +492,8 @@
   39.16  val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
   39.17  
   39.18  fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
   39.19 -  REPEAT_ALL_NEW (rtac quant_inst_rule)
   39.20 -  THEN' rtac @{thm excluded_middle})
   39.21 +  REPEAT_ALL_NEW (resolve_tac ctxt [quant_inst_rule])
   39.22 +  THEN' resolve_tac ctxt @{thms excluded_middle})
   39.23  
   39.24  
   39.25  (* propositional lemma *)
    40.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Sat Jul 18 20:37:16 2015 +0200
    40.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Sat Jul 18 20:47:08 2015 +0200
    40.3 @@ -627,7 +627,7 @@
    40.4  
    40.5  fun eq_rules_tac ctxt eq_rules =
    40.6    TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules)
    40.7 -  THEN_ALL_NEW rtac @{thm is_equality_eq}
    40.8 +  THEN_ALL_NEW resolve_tac ctxt @{thms is_equality_eq}
    40.9  
   40.10  fun eq_tac ctxt = eq_rules_tac ctxt (get_relator_eq_raw ctxt)
   40.11  
   40.12 @@ -646,8 +646,8 @@
   40.13      val end_tac = if equiv then K all_tac else K no_tac
   40.14      val err_msg = "Transfer failed to convert goal to an object-logic formula"
   40.15      fun main_tac (t, i) =
   40.16 -      rtac start_rule i THEN
   40.17 -      (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
   40.18 +      resolve_tac ctxt [start_rule] i THEN
   40.19 +      (resolve_tac ctxt [transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)]
   40.20          THEN_ALL_NEW
   40.21            (SOLVED'
   40.22              (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
   40.23 @@ -673,12 +673,13 @@
   40.24    in
   40.25      EVERY
   40.26        [CONVERSION prep_conv i,
   40.27 -       rtac @{thm transfer_prover_start} i,
   40.28 -       ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
   40.29 +       resolve_tac ctxt @{thms transfer_prover_start} i,
   40.30 +       ((resolve_tac ctxt [rule1] ORELSE'
   40.31 +         (CONVERSION expand_eq_in_rel THEN' resolve_tac ctxt [rule1]))
   40.32          THEN_ALL_NEW
   40.33           (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
   40.34             (DETERM o eq_rules_tac ctxt eq_rules))) (i + 1),
   40.35 -       rtac @{thm refl} i]
   40.36 +       resolve_tac ctxt @{thms refl} i]
   40.37    end)
   40.38  
   40.39  (** Transfer attribute **)
   40.40 @@ -702,7 +703,7 @@
   40.41      val rule = transfer_rule_of_lhs ctxt' t
   40.42      val tac =
   40.43        resolve_tac ctxt' [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
   40.44 -      (rtac rule
   40.45 +      (resolve_tac ctxt' [rule]
   40.46          THEN_ALL_NEW
   40.47            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
   40.48              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
   40.49 @@ -737,8 +738,8 @@
   40.50      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
   40.51      val rule = transfer_rule_of_term ctxt' true t
   40.52      val tac =
   40.53 -      rtac (thm2 RS start_rule) 1 THEN
   40.54 -      (rtac rule
   40.55 +      resolve_tac ctxt' [thm2 RS start_rule] 1 THEN
   40.56 +      (resolve_tac ctxt' [rule]
   40.57          THEN_ALL_NEW
   40.58            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
   40.59              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
    41.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sat Jul 18 20:37:16 2015 +0200
    41.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Jul 18 20:47:08 2015 +0200
    41.3 @@ -113,11 +113,11 @@
    41.4          (fn prems =>
    41.5             EVERY [
    41.6              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
    41.7 -            rtac (cterm_instantiate inst induct) 1,
    41.8 +            resolve_tac ctxt [cterm_instantiate inst induct] 1,
    41.9              ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
   41.10              rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
   41.11              REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i =>
   41.12 -              REPEAT (etac allE i) THEN assume_tac ctxt i)) 1)])
   41.13 +              REPEAT (eresolve_tac ctxt [allE] i) THEN assume_tac ctxt i)) 1)])
   41.14        |> Drule.export_without_context;
   41.15  
   41.16      val ind_name = Thm.derivation_name induct;
   41.17 @@ -190,7 +190,7 @@
   41.18            (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
   41.19          (fn prems =>
   41.20             EVERY [
   41.21 -            rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust) 1,
   41.22 +            resolve_tac ctxt [cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust] 1,
   41.23              ALLGOALS (EVERY'
   41.24                [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
   41.25                 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
    42.1 --- a/src/HOL/Tools/groebner.ML	Sat Jul 18 20:37:16 2015 +0200
    42.2 +++ b/src/HOL/Tools/groebner.ML	Sat Jul 18 20:47:08 2015 +0200
    42.3 @@ -931,11 +931,11 @@
    42.4    Object_Logic.full_atomize_tac ctxt
    42.5    THEN' presimplify ctxt add_ths del_ths
    42.6    THEN' CSUBGOAL (fn (p, i) =>
    42.7 -    rtac (let val form = Object_Logic.dest_judgment ctxt p
    42.8 +    resolve_tac ctxt [let val form = Object_Logic.dest_judgment ctxt p
    42.9            in case get_ring_ideal_convs ctxt form of
   42.10             NONE => Thm.reflexive form
   42.11            | SOME thy => #ring_conv thy ctxt form
   42.12 -          end) i
   42.13 +          end] i
   42.14        handle TERM _ => no_tac
   42.15          | CTERM _ => no_tac
   42.16          | THM _ => no_tac);
   42.17 @@ -944,8 +944,9 @@
   42.18   fun lhs t = case Thm.term_of t of
   42.19    Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
   42.20   | _=> raise CTERM ("ideal_tac - lhs",[t])
   42.21 - fun exitac NONE = no_tac
   42.22 -   | exitac (SOME y) = rtac (instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI) 1
   42.23 + fun exitac _ NONE = no_tac
   42.24 +   | exitac ctxt (SOME y) =
   42.25 +      resolve_tac ctxt [instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
   42.26  
   42.27   val claset = claset_of @{context}
   42.28  in
   42.29 @@ -964,7 +965,7 @@
   42.30       val ps = map_filter (try (lhs o Thm.dest_arg)) asms
   42.31       val cfs = (map swap o #multi_ideal thy evs ps)
   42.32                     (map Thm.dest_arg1 (conjuncts bod))
   42.33 -     val ws = map (exitac o AList.lookup op aconvc cfs) evs
   42.34 +     val ws = map (exitac ctxt o AList.lookup op aconvc cfs) evs
   42.35      in EVERY (rev ws) THEN Method.insert_tac prems 1
   42.36          THEN ring_tac add_ths del_ths ctxt 1
   42.37     end
    43.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Jul 18 20:37:16 2015 +0200
    43.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jul 18 20:47:08 2015 +0200
    43.3 @@ -393,11 +393,12 @@
    43.4          val thm = Goal.prove_global thy []
    43.5            (map attach_typeS prems) (attach_typeS concl)
    43.6            (fn {context = ctxt, prems} => EVERY
    43.7 -          [rtac (#raw_induct ind_info) 1,
    43.8 +          [resolve_tac ctxt [#raw_induct ind_info] 1,
    43.9             rewrite_goals_tac ctxt rews,
   43.10             REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW EVERY'
   43.11               [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
   43.12 -              DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE]]) 1)]);
   43.13 +              DEPTH_SOLVE_1 o
   43.14 +              FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]]]) 1)]);
   43.15          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   43.16            (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
   43.17          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   43.18 @@ -456,11 +457,12 @@
   43.19            (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz')
   43.20            (fn {context = ctxt, prems, ...} => EVERY
   43.21              [cut_tac (hd prems) 1,
   43.22 -             etac elimR 1,
   43.23 +             eresolve_tac ctxt [elimR] 1,
   43.24               ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
   43.25               rewrite_goals_tac ctxt rews,
   43.26               REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
   43.27 -               DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE])) 1)]);
   43.28 +               DEPTH_SOLVE_1 o
   43.29 +               FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]])) 1)]);
   43.30          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   43.31            (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
   43.32        in
    44.1 --- a/src/HOL/Tools/record.ML	Sat Jul 18 20:37:16 2015 +0200
    44.2 +++ b/src/HOL/Tools/record.ML	Sat Jul 18 20:47:08 2015 +0200
    44.3 @@ -112,7 +112,7 @@
    44.4    in
    44.5      thy
    44.6      |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
    44.7 -        (HOLogic.mk_UNIV repT) NONE (fn _ => rtac UNIV_witness 1)
    44.8 +        (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
    44.9      |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   44.10    end;
   44.11  
   44.12 @@ -184,7 +184,7 @@
   44.13          (case Symtab.lookup isthms (#1 is) of
   44.14            SOME isthm => isthm
   44.15          | NONE => err "no thm found for constant" (Const is));
   44.16 -    in rtac isthm i end);
   44.17 +    in resolve_tac ctxt [isthm] i end);
   44.18  
   44.19  end;
   44.20  
   44.21 @@ -1380,7 +1380,7 @@
   44.22          val thm = cterm_instantiate [(crec, cfree)] induct_thm;
   44.23        in
   44.24          simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN
   44.25 -        rtac thm i THEN
   44.26 +        resolve_tac ctxt [thm] i THEN
   44.27          simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_rulify}) i
   44.28        end;
   44.29  
   44.30 @@ -1591,9 +1591,9 @@
   44.31            (fn {context = ctxt, ...} =>
   44.32              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
   44.33              REPEAT_DETERM
   44.34 -              (rtac @{thm refl_conj_eq} 1 ORELSE
   44.35 +              (resolve_tac ctxt @{thms refl_conj_eq} 1 ORELSE
   44.36                  Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
   44.37 -                rtac refl 1))));
   44.38 +                resolve_tac ctxt [refl] 1))));
   44.39  
   44.40  
   44.41      (*We need a surjection property r = (| f = f r, g = g r ... |)
   44.42 @@ -1610,7 +1610,8 @@
   44.43          val tactic1 =
   44.44            simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
   44.45            REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1;
   44.46 -        val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   44.47 +        val tactic2 =
   44.48 +          REPEAT (resolve_tac defs_ctxt [surject_assistI] 1 THEN resolve_tac defs_ctxt [refl] 1);
   44.49          val [halfway] = Seq.list_of (tactic1 start);
   44.50          val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
   44.51        in
   44.52 @@ -1621,10 +1622,11 @@
   44.53        Goal.prove_sorry_global defs_thy [] [] split_meta_prop
   44.54          (fn {context = ctxt, ...} =>
   44.55            EVERY1
   44.56 -           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
   44.57 -            etac @{thm meta_allE}, assume_tac ctxt,
   44.58 -            rtac (@{thm prop_subst} OF [surject]),
   44.59 -            REPEAT o etac @{thm meta_allE}, assume_tac ctxt]));
   44.60 +           [resolve_tac ctxt @{thms equal_intr_rule},
   44.61 +            Goal.norm_hhf_tac ctxt,
   44.62 +            eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt,
   44.63 +            resolve_tac ctxt [@{thm prop_subst} OF [surject]],
   44.64 +            REPEAT o eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt]));
   44.65  
   44.66      val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
   44.67        let val (assm, concl) = induct_prop in
   44.68 @@ -1748,7 +1750,7 @@
   44.69        fun tac ctxt eq_def =
   44.70          Class.intro_classes_tac ctxt []
   44.71          THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
   44.72 -        THEN ALLGOALS (rtac @{thm refl});
   44.73 +        THEN ALLGOALS (resolve_tac ctxt @{thms refl});
   44.74        fun mk_eq thy eq_def =
   44.75          rewrite_rule (Proof_Context.init_global thy)
   44.76            [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
   44.77 @@ -1946,7 +1948,8 @@
   44.78            val cterm_vrs = Thm.cterm_of ext_ctxt r_rec0_Vars;
   44.79            val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
   44.80            val init_thm = named_cterm_instantiate insts updacc_eq_triv;
   44.81 -          val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   44.82 +          val terminal =
   44.83 +            resolve_tac ext_ctxt [updacc_eq_idI] 1 THEN resolve_tac ext_ctxt [refl] 1;
   44.84            val tactic =
   44.85              simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN
   44.86              REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac ext_ctxt 1 ORELSE terminal);
   44.87 @@ -2131,11 +2134,11 @@
   44.88        Goal.prove_sorry_global defs_thy [] [] surjective_prop
   44.89          (fn {context = ctxt, ...} =>
   44.90            EVERY
   44.91 -           [rtac surject_assist_idE 1,
   44.92 +           [resolve_tac ctxt [surject_assist_idE] 1,
   44.93              simp_tac (put_simpset HOL_basic_ss ctxt addsimps ext_defs) 1,
   44.94              REPEAT
   44.95                (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
   44.96 -                (rtac surject_assistI 1 THEN
   44.97 +                (resolve_tac ctxt [surject_assistI] 1 THEN
   44.98                    simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt
   44.99                      addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))]));
  44.100  
  44.101 @@ -2143,7 +2146,7 @@
  44.102        Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
  44.103          (fn {context = ctxt, prems, ...} =>
  44.104            resolve_tac ctxt prems 1 THEN
  44.105 -          rtac surjective 1));
  44.106 +          resolve_tac ctxt [surjective] 1));
  44.107  
  44.108      val cases = timeit_msg ctxt "record cases proof:" (fn () =>
  44.109        Goal.prove_sorry_global defs_thy [] [] cases_prop
  44.110 @@ -2156,26 +2159,26 @@
  44.111        Goal.prove_sorry_global defs_thy [] [] split_meta_prop
  44.112          (fn {context = ctxt', ...} =>
  44.113            EVERY1
  44.114 -           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
  44.115 -            etac @{thm meta_allE}, assume_tac ctxt',
  44.116 -            rtac (@{thm prop_subst} OF [surjective]),
  44.117 -            REPEAT o etac @{thm meta_allE}, assume_tac ctxt']));
  44.118 +           [resolve_tac ctxt' @{thms equal_intr_rule}, Goal.norm_hhf_tac ctxt',
  44.119 +            eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt',
  44.120 +            resolve_tac ctxt' [@{thm prop_subst} OF [surjective]],
  44.121 +            REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt']));
  44.122  
  44.123      val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
  44.124        Goal.prove_sorry_global defs_thy [] [] split_object_prop
  44.125          (fn {context = ctxt, ...} =>
  44.126 -          rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
  44.127 +          resolve_tac ctxt [@{lemma "Trueprop A \<equiv> Trueprop B \<Longrightarrow> A = B" by (rule iffI) unfold}] 1 THEN
  44.128            rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
  44.129 -          rtac split_meta 1));
  44.130 +          resolve_tac ctxt [split_meta] 1));
  44.131  
  44.132      val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
  44.133        Goal.prove_sorry_global defs_thy [] [] split_ex_prop
  44.134          (fn {context = ctxt, ...} =>
  44.135            simp_tac
  44.136              (put_simpset HOL_basic_ss ctxt addsimps
  44.137 -              (@{lemma "EX x. P x == ~ (ALL x. ~ P x)" by simp} ::
  44.138 +              (@{lemma "\<exists>x. P x \<equiv> \<not> (\<forall>x. \<not> P x)" by simp} ::
  44.139                  @{thms not_not Not_eq_iff})) 1 THEN
  44.140 -          rtac split_object 1));
  44.141 +          resolve_tac ctxt [split_object] 1));
  44.142  
  44.143      val equality = timeit_msg ctxt "record equality proof:" (fn () =>
  44.144        Goal.prove_sorry_global defs_thy [] [] equality_prop
    45.1 --- a/src/HOL/Tools/reification.ML	Sat Jul 18 20:37:16 2015 +0200
    45.2 +++ b/src/HOL/Tools/reification.ML	Sat Jul 18 20:47:08 2015 +0200
    45.3 @@ -32,7 +32,7 @@
    45.4      val thm = conv ct;
    45.5    in
    45.6      if Thm.is_reflexive thm then no_tac
    45.7 -    else ALLGOALS (rtac (pure_subst OF [thm]))
    45.8 +    else ALLGOALS (resolve_tac ctxt [pure_subst OF [thm]])
    45.9    end) ctxt;
   45.10  
   45.11  (* Make a congruence rule out of a defining equation for the interpretation
   45.12 @@ -82,7 +82,7 @@
   45.13        (Goal.prove ctxt'' [] (map mk_def env)
   45.14          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
   45.15          (fn {context, prems, ...} =>
   45.16 -          Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym;
   45.17 +          Local_Defs.unfold_tac context (map tryext prems) THEN resolve_tac ctxt'' [th'] 1)) RS sym;
   45.18      val (cong' :: vars') =
   45.19        Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Thm.cterm_of ctxt'') vs);
   45.20      val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';