eliminated aliases;
authorwenzelm
Thu Oct 30 16:55:29 2014 +0100 (2014-10-30)
changeset 5883859203adfc33f
parent 58837 e84d900cd287
child 58839 ccda99401bc8
eliminated aliases;
src/FOL/ex/Miniscope.thy
src/FOL/simpdata.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/hypsubst.ML
src/Provers/quantifier1.ML
src/Provers/splitter.ML
src/Tools/case_product.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
src/ZF/Datatype_ZF.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/Tools/typechk.ML
src/ZF/arith_data.ML
     1.1 --- a/src/FOL/ex/Miniscope.thy	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/FOL/ex/Miniscope.thy	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4  
     1.5  ML {*
     1.6  val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
     1.7 -fun mini_tac ctxt = rtac @{thm ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
     1.8 +fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
     1.9  *}
    1.10  
    1.11  end
     2.1 --- a/src/FOL/simpdata.ML	Thu Oct 30 16:20:46 2014 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Thu Oct 30 16:55:29 2014 +0100
     2.3 @@ -107,7 +107,9 @@
     2.4  val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
     2.5  
     2.6  fun unsafe_solver ctxt =
     2.7 -  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), atac, etac @{thm FalseE}];
     2.8 +  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt),
     2.9 +    assume_tac,
    2.10 +    eresolve_tac @{thms FalseE}];
    2.11  
    2.12  (*No premature instantiation of variables during simplification*)
    2.13  fun safe_solver ctxt =
     3.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 16:20:46 2014 +0100
     3.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 16:55:29 2014 +0100
     3.3 @@ -92,12 +92,12 @@
     3.4      Option.map (export o Data.simplify_meta_eq ctxt)
     3.5        (if n2 <= n1 then
     3.6           Data.prove_conv
     3.7 -           [Data.trans_tac reshape, rtac Data.bal_add1 1,
     3.8 +           [Data.trans_tac reshape, resolve_tac [Data.bal_add1] 1,
     3.9              Data.numeral_simp_tac ctxt] ctxt prems
    3.10             (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
    3.11         else
    3.12           Data.prove_conv
    3.13 -           [Data.trans_tac reshape, rtac Data.bal_add2 1,
    3.14 +           [Data.trans_tac reshape, resolve_tac [Data.bal_add2] 1,
    3.15              Data.numeral_simp_tac ctxt] ctxt prems
    3.16             (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
    3.17    end
     4.1 --- a/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 16:20:46 2014 +0100
     4.2 +++ b/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 16:55:29 2014 +0100
     4.3 @@ -83,7 +83,7 @@
     4.4    in
     4.5      Option.map (export o Data.simplify_meta_eq ctxt)
     4.6        (Data.prove_conv
     4.7 -         [Data.trans_tac reshape, rtac Data.left_distrib 1,
     4.8 +         [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1,
     4.9            Data.numeral_simp_tac ctxt] ctxt
    4.10           (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    4.11    end
     5.1 --- a/src/Provers/blast.ML	Thu Oct 30 16:20:46 2014 +0100
     5.2 +++ b/src/Provers/blast.ML	Thu Oct 30 16:55:29 2014 +0100
     5.3 @@ -488,8 +488,8 @@
     5.4  
     5.5  (*Resolution/matching tactics: if upd then the proof state may be updated.
     5.6    Matching makes the tactics more deterministic in the presence of Vars.*)
     5.7 -fun emtac ctxt upd rl = TRACE ctxt rl (if upd then etac rl else ematch_tac [rl]);
     5.8 -fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then rtac rl else match_tac [rl]);
     5.9 +fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]);
    5.10 +fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]);
    5.11  
    5.12  (*Tableau rule from elimination rule.
    5.13    Flag "upd" says that the inference updated the branch.
    5.14 @@ -624,7 +624,7 @@
    5.15  
    5.16  (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
    5.17  fun negOfGoal_tac ctxt i =
    5.18 -  TRACE ctxt Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i;
    5.19 +  TRACE ctxt Data.ccontr (resolve_tac [Data.ccontr]) i THEN rotate_tac ~1 i;
    5.20  
    5.21  fun traceTerm ctxt t =
    5.22    let val thy = Proof_Context.theory_of ctxt
     6.1 --- a/src/Provers/classical.ML	Thu Oct 30 16:20:46 2014 +0100
     6.2 +++ b/src/Provers/classical.ML	Thu Oct 30 16:55:29 2014 +0100
     6.3 @@ -157,7 +157,7 @@
     6.4        val rule'' =
     6.5          rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
     6.6            if i = 1 orelse redundant_hyp goal
     6.7 -          then etac thin_rl i
     6.8 +          then eresolve_tac [thin_rl] i
     6.9            else all_tac))
    6.10          |> Seq.hd
    6.11          |> Drule.zero_var_indexes;
    6.12 @@ -209,7 +209,7 @@
    6.13    let
    6.14      val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    6.15      val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
    6.16 -  in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
    6.17 +  in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end;
    6.18  
    6.19  
    6.20  (**** Classical rule sets ****)
    6.21 @@ -689,8 +689,8 @@
    6.22  fun ctxt addafter (name, tac2) =
    6.23    ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
    6.24  
    6.25 -fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dtac thm THEN' assume_tac);
    6.26 -fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => etac thm THEN' assume_tac);
    6.27 +fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
    6.28 +fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
    6.29  fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
    6.30  fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
    6.31  
    6.32 @@ -909,7 +909,7 @@
    6.33      val ruleq = Drule.multi_resolves facts rules;
    6.34      val _ = Method.trace ctxt rules;
    6.35    in
    6.36 -    fn st => Seq.maps (fn rule => rtac rule i st) ruleq
    6.37 +    fn st => Seq.maps (fn rule => resolve_tac [rule] i st) ruleq
    6.38    end)
    6.39    THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
    6.40  
     7.1 --- a/src/Provers/hypsubst.ML	Thu Oct 30 16:20:46 2014 +0100
     7.2 +++ b/src/Provers/hypsubst.ML	Thu Oct 30 16:55:29 2014 +0100
     7.3 @@ -126,7 +126,7 @@
     7.4       val (k, _) = eq_var false false false t
     7.5       val ok = (eq_var false false true t |> fst) > k
     7.6          handle EQ_VAR => true
     7.7 -   in if ok then EVERY [rotate_tac k i, etac thin_rl i, rotate_tac (~k) i]
     7.8 +   in if ok then EVERY [rotate_tac k i, eresolve_tac [thin_rl] i, rotate_tac (~k) i]
     7.9      else no_tac
    7.10     end handle EQ_VAR => no_tac)
    7.11  
    7.12 @@ -151,11 +151,11 @@
    7.13          val (k, (orient, is_free)) = eq_var bnd true true Bi
    7.14          val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
    7.15        in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
    7.16 -        if not is_free then etac thin_rl i
    7.17 -          else if orient then etac Data.rev_mp i
    7.18 -          else etac (Data.sym RS Data.rev_mp) i,
    7.19 +        if not is_free then eresolve_tac [thin_rl] i
    7.20 +          else if orient then eresolve_tac [Data.rev_mp] i
    7.21 +          else eresolve_tac [Data.sym RS Data.rev_mp] i,
    7.22          rotate_tac (~k) i,
    7.23 -        if is_free then rtac Data.imp_intr i else all_tac]
    7.24 +        if is_free then resolve_tac [Data.imp_intr] i else all_tac]
    7.25        end handle THM _ => no_tac | EQ_VAR => no_tac)
    7.26  
    7.27  end;
    7.28 @@ -194,7 +194,7 @@
    7.29        end
    7.30    | NONE => no_tac);
    7.31  
    7.32 -val imp_intr_tac = rtac Data.imp_intr;
    7.33 +val imp_intr_tac = resolve_tac [Data.imp_intr];
    7.34  
    7.35  fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    7.36  val dup_subst = rev_dup_elim ssubst
    7.37 @@ -211,9 +211,9 @@
    7.38            val rl = if orient then rl else Data.sym RS rl
    7.39        in
    7.40           DETERM
    7.41 -           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
    7.42 +           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
    7.43                     rotate_tac 1 i,
    7.44 -                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
    7.45 +                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
    7.46                     inst_subst_tac orient rl i,
    7.47                     REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
    7.48        end
    7.49 @@ -245,7 +245,7 @@
    7.50  fun reverse_n_tac 0 i = all_tac
    7.51    | reverse_n_tac 1 i = rotate_tac ~1 i
    7.52    | reverse_n_tac n i =
    7.53 -      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
    7.54 +      REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac [Data.rev_mp] i) THEN
    7.55        REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
    7.56  
    7.57  (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
    7.58 @@ -279,9 +279,9 @@
    7.59        in
    7.60           if trace then tracing "Substituting an equality" else ();
    7.61           DETERM
    7.62 -           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
    7.63 +           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
    7.64                     rotate_tac 1 i,
    7.65 -                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
    7.66 +                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
    7.67                     inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
    7.68                     all_imp_intr_tac hyps i])
    7.69        end
    7.70 @@ -291,7 +291,7 @@
    7.71    fails unless the substitution has an effect*)
    7.72  fun stac th =
    7.73    let val th' = th RS Data.rev_eq_reflection handle THM _ => th
    7.74 -  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
    7.75 +  in CHANGED_GOAL (resolve_tac [th' RS ssubst]) end;
    7.76  
    7.77  
    7.78  (* method setup *)
     8.1 --- a/src/Provers/quantifier1.ML	Thu Oct 30 16:20:46 2014 +0100
     8.2 +++ b/src/Provers/quantifier1.ML	Thu Oct 30 16:55:29 2014 +0100
     8.3 @@ -126,10 +126,10 @@
     8.4        yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
     8.5      val thm =
     8.6        Goal.prove ctxt' [] [] goal
     8.7 -        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
     8.8 +        (fn {context = ctxt'', ...} => resolve_tac [Data.iff_reflection] 1 THEN tac ctxt'');
     8.9    in singleton (Variable.export ctxt' ctxt) thm end;
    8.10  
    8.11 -fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
    8.12 +fun qcomm_tac qcomm qI i = REPEAT_DETERM (resolve_tac [qcomm] i THEN resolve_tac [qI] i);
    8.13  
    8.14  (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
    8.15     Better: instantiate exI
    8.16 @@ -138,9 +138,10 @@
    8.17    val excomm = Data.ex_comm RS Data.iff_trans;
    8.18  in
    8.19    val prove_one_point_ex_tac =
    8.20 -    qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
    8.21 +    qcomm_tac excomm Data.iff_exI 1 THEN resolve_tac [Data.iffI] 1 THEN
    8.22      ALLGOALS
    8.23 -      (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI,
    8.24 +      (EVERY' [eresolve_tac [Data.exE], REPEAT_DETERM o eresolve_tac [Data.conjE],
    8.25 +        resolve_tac [Data.exI],
    8.26          DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
    8.27  end;
    8.28  
    8.29 @@ -150,12 +151,17 @@
    8.30  local
    8.31    val tac =
    8.32      SELECT_GOAL
    8.33 -      (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp,
    8.34 -        REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]);
    8.35 +      (EVERY1 [REPEAT o dresolve_tac [Data.uncurry],
    8.36 +        REPEAT o resolve_tac [Data.impI],
    8.37 +        eresolve_tac [Data.mp],
    8.38 +        REPEAT o eresolve_tac [Data.conjE],
    8.39 +        REPEAT o ares_tac [Data.conjI]]);
    8.40    val allcomm = Data.all_comm RS Data.iff_trans;
    8.41  in
    8.42    val prove_one_point_all_tac =
    8.43 -    EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac];
    8.44 +    EVERY1 [qcomm_tac allcomm Data.iff_allI,
    8.45 +      resolve_tac [Data.iff_allI],
    8.46 +      resolve_tac [Data.iffI], tac, tac];
    8.47  end
    8.48  
    8.49  fun renumber l u (Bound i) =
     9.1 --- a/src/Provers/splitter.ML	Thu Oct 30 16:20:46 2014 +0100
     9.2 +++ b/src/Provers/splitter.ML	Thu Oct 30 16:55:29 2014 +0100
     9.3 @@ -99,7 +99,7 @@
     9.4  val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
     9.5    [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
     9.6    (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
     9.7 -  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
     9.8 +  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN resolve_tac [reflexive_thm] 1)
     9.9  
    9.10  val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
    9.11  
    9.12 @@ -365,11 +365,11 @@
    9.13                     (case apsns of
    9.14                        [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
    9.15                      | p::_ => EVERY [lift_tac Ts t p,
    9.16 -                                     rtac reflexive_thm (i+1),
    9.17 +                                     resolve_tac [reflexive_thm] (i+1),
    9.18                                       lift_split_tac] state)
    9.19              end
    9.20    in COND (has_fewer_prems i) no_tac
    9.21 -          (rtac meta_iffD i THEN lift_split_tac)
    9.22 +          (resolve_tac [meta_iffD] i THEN lift_split_tac)
    9.23    end;
    9.24  
    9.25  in (split_tac, exported_split_posns) end;  (* mk_case_split_tac *)
    9.26 @@ -400,16 +400,16 @@
    9.27        (* does not work properly if the split variable is bound by a quantifier *)
    9.28                fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
    9.29                             (if first_prem_is_disj t
    9.30 -                            then EVERY[etac Data.disjE i,rotate_tac ~1 i,
    9.31 +                            then EVERY[eresolve_tac [Data.disjE] i, rotate_tac ~1 i,
    9.32                                         rotate_tac ~1  (i+1),
    9.33                                         flat_prems_tac (i+1)]
    9.34                              else all_tac)
    9.35                             THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
    9.36                             THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
    9.37            in if n<0 then  no_tac  else (DETERM (EVERY'
    9.38 -                [rotate_tac n, etac Data.contrapos2,
    9.39 +                [rotate_tac n, eresolve_tac [Data.contrapos2],
    9.40                   split_tac splits,
    9.41 -                 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
    9.42 +                 rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1,
    9.43                   flat_prems_tac] i))
    9.44            end;
    9.45    in SUBGOAL tac
    10.1 --- a/src/Tools/case_product.ML	Thu Oct 30 16:20:46 2014 +0100
    10.2 +++ b/src/Tools/case_product.ML	Thu Oct 30 16:55:29 2014 +0100
    10.3 @@ -70,9 +70,9 @@
    10.4      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
    10.5      val thm2' = thm2 OF p_cons2
    10.6    in
    10.7 -    rtac (thm1 OF p_cons1)
    10.8 +    resolve_tac [thm1 OF p_cons1]
    10.9       THEN' EVERY' (map (fn p =>
   10.10 -       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
   10.11 +       resolve_tac [thm2'] THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
   10.12    end
   10.13  
   10.14  fun combine ctxt thm1 thm2 =
    11.1 --- a/src/Tools/eqsubst.ML	Thu Oct 30 16:20:46 2014 +0100
    11.2 +++ b/src/Tools/eqsubst.ML	Thu Oct 30 16:55:29 2014 +0100
    11.3 @@ -250,7 +250,7 @@
    11.4    RW_Inst.rw ctxt m rule conclthm
    11.5    |> unfix_frees cfvs
    11.6    |> Conv.fconv_rule Drule.beta_eta_conversion
    11.7 -  |> (fn r => rtac r i st);
    11.8 +  |> (fn r => resolve_tac [r] i st);
    11.9  
   11.10  (* substitute within the conclusion of goal i of gth, using a meta
   11.11  equation rule. Note that we assume rule has var indicies zero'd *)
   11.12 @@ -332,7 +332,7 @@
   11.13        |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
   11.14    in
   11.15      (* ~j because new asm starts at back, thus we subtract 1 *)
   11.16 -    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
   11.17 +    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dresolve_tac [preelimrule] i st2)
   11.18    end;
   11.19  
   11.20  
    12.1 --- a/src/Tools/induct.ML	Thu Oct 30 16:20:46 2014 +0100
    12.2 +++ b/src/Tools/induct.ML	Thu Oct 30 16:55:29 2014 +0100
    12.3 @@ -512,7 +512,7 @@
    12.4          in
    12.5            CASES (Rule_Cases.make_common (thy,
    12.6                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
    12.7 -            ((Method.insert_tac more_facts THEN' rtac rule' THEN_ALL_NEW
    12.8 +            ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
    12.9                  (if simp then TRY o trivial_tac else K all_tac)) i) st
   12.10          end)
   12.11    end;
   12.12 @@ -683,7 +683,8 @@
   12.13    in
   12.14      (case goal_concl n [] goal of
   12.15        SOME concl =>
   12.16 -        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
   12.17 +        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
   12.18 +          resolve_tac [asm_rl]) i
   12.19      | NONE => all_tac)
   12.20    end);
   12.21  
   12.22 @@ -804,7 +805,7 @@
   12.23                |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   12.24                |> Seq.maps (fn rule' =>
   12.25                  CASES (rule_cases ctxt rule' cases)
   12.26 -                  (rtac rule' i THEN
   12.27 +                  (resolve_tac [rule'] i THEN
   12.28                      PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
   12.29        end)
   12.30        THEN_ALL_NEW_CASES
   12.31 @@ -862,7 +863,7 @@
   12.32          |> Seq.maps (fn rule' =>
   12.33            CASES (Rule_Cases.make_common (thy,
   12.34                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   12.35 -            (Method.insert_tac more_facts i THEN rtac rule' i) st))
   12.36 +            (Method.insert_tac more_facts i THEN resolve_tac [rule'] i) st))
   12.37    end);
   12.38  
   12.39  end;
    13.1 --- a/src/ZF/Datatype_ZF.thy	Thu Oct 30 16:20:46 2014 +0100
    13.2 +++ b/src/ZF/Datatype_ZF.thy	Thu Oct 30 16:55:29 2014 +0100
    13.3 @@ -95,7 +95,7 @@
    13.4           else ();
    13.5         val goal = Logic.mk_equals (old, new)
    13.6         val thm = Goal.prove ctxt [] [] goal
    13.7 -         (fn _ => rtac @{thm iff_reflection} 1 THEN
    13.8 +         (fn _ => resolve_tac @{thms iff_reflection} 1 THEN
    13.9             simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1)
   13.10           handle ERROR msg =>
   13.11           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
    14.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Oct 30 16:20:46 2014 +0100
    14.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Oct 30 16:55:29 2014 +0100
    14.3 @@ -289,7 +289,7 @@
    14.4        (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
    14.5        (fn {context = ctxt, ...} => EVERY
    14.6          [rewrite_goals_tac ctxt [con_def],
    14.7 -         rtac case_trans 1,
    14.8 +         resolve_tac [case_trans] 1,
    14.9           REPEAT
   14.10             (resolve_tac [@{thm refl}, split_trans,
   14.11               Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]);
   14.12 @@ -330,7 +330,7 @@
   14.13              (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg))
   14.14              (*Proves a single recursor equation.*)
   14.15              (fn {context = ctxt, ...} => EVERY
   14.16 -              [rtac recursor_trans 1,
   14.17 +              [resolve_tac [recursor_trans] 1,
   14.18                 simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1,
   14.19                 IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]);
   14.20        in
    15.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Oct 30 16:20:46 2014 +0100
    15.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 30 16:55:29 2014 +0100
    15.3 @@ -189,7 +189,7 @@
    15.4    val bnd_mono =
    15.5      Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
    15.6        (fn _ => EVERY
    15.7 -        [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
    15.8 +        [resolve_tac [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
    15.9           REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
   15.10  
   15.11    val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
   15.12 @@ -218,13 +218,13 @@
   15.13      [DETERM (stac unfold 1),
   15.14       REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
   15.15       (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
   15.16 -     rtac disjIn 2,
   15.17 +     resolve_tac [disjIn] 2,
   15.18       (*Not ares_tac, since refl must be tried before equality assumptions;
   15.19         backtracking may occur if the premises have extra variables!*)
   15.20       DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
   15.21       (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
   15.22       rewrite_goals_tac ctxt con_defs,
   15.23 -     REPEAT (rtac @{thm refl} 2),
   15.24 +     REPEAT (resolve_tac @{thms refl} 2),
   15.25       (*Typechecking; this can fail*)
   15.26       if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
   15.27       else all_tac,
   15.28 @@ -332,15 +332,15 @@
   15.29             setSolver (mk_solver "minimal"
   15.30                        (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)
   15.31                                     ORELSE' assume_tac
   15.32 -                                   ORELSE' etac @{thm FalseE}));
   15.33 +                                   ORELSE' eresolve_tac @{thms FalseE}));
   15.34  
   15.35       val quant_induct =
   15.36         Goal.prove_global thy1 [] ind_prems
   15.37           (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
   15.38           (fn {context = ctxt, prems} => EVERY
   15.39             [rewrite_goals_tac ctxt part_rec_defs,
   15.40 -            rtac (@{thm impI} RS @{thm allI}) 1,
   15.41 -            DETERM (etac raw_induct 1),
   15.42 +            resolve_tac [@{thm impI} RS @{thm allI}] 1,
   15.43 +            DETERM (eresolve_tac [raw_induct] 1),
   15.44              (*Push Part inside Collect*)
   15.45              full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
   15.46              (*This CollectE and disjE separates out the introduction rules*)
   15.47 @@ -470,8 +470,8 @@
   15.48                        (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
   15.49                     THEN
   15.50                     (*unpackage and use "prem" in the corresponding place*)
   15.51 -                   REPEAT (rtac @{thm impI} 1)  THEN
   15.52 -                   rtac (rewrite_rule ctxt all_defs prem) 1  THEN
   15.53 +                   REPEAT (resolve_tac @{thms impI} 1)  THEN
   15.54 +                   resolve_tac [rewrite_rule ctxt all_defs prem] 1  THEN
   15.55                     (*prem must not be REPEATed below: could loop!*)
   15.56                     DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
   15.57                                             eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
   15.58 @@ -483,7 +483,7 @@
   15.59           Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
   15.60             mutual_induct_concl
   15.61             (fn {context = ctxt, prems} => EVERY
   15.62 -             [rtac (quant_induct RS lemma) 1,
   15.63 +             [resolve_tac [quant_induct RS lemma] 1,
   15.64                mutual_ind_tac ctxt (rev prems) (length prems)])
   15.65         else @{thm TrueI};
   15.66  
    16.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Oct 30 16:20:46 2014 +0100
    16.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Oct 30 16:55:29 2014 +0100
    16.3 @@ -176,7 +176,8 @@
    16.4      val eqn_thms =
    16.5        eqn_terms |> map (fn t =>
    16.6          Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
    16.7 -          (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
    16.8 +          (fn {context = ctxt, ...} =>
    16.9 +            EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac @{thms refl} 1]));
   16.10  
   16.11      val (eqn_thms', thy2) =
   16.12        thy1
    17.1 --- a/src/ZF/Tools/typechk.ML	Thu Oct 30 16:20:46 2014 +0100
    17.2 +++ b/src/ZF/Tools/typechk.ML	Thu Oct 30 16:55:29 2014 +0100
    17.3 @@ -99,7 +99,7 @@
    17.4  (*Instantiates variables in typing conditions.
    17.5    drawback: does not simplify conjunctions*)
    17.6  fun type_solver_tac ctxt hyps = SELECT_GOAL
    17.7 -    (DEPTH_SOLVE (etac @{thm FalseE} 1
    17.8 +    (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
    17.9                    ORELSE basic_res_tac 1
   17.10                    ORELSE (ares_tac hyps 1
   17.11                            APPEND typecheck_step_tac (tcset_of ctxt))));
    18.1 --- a/src/ZF/arith_data.ML	Thu Oct 30 16:20:46 2014 +0100
    18.2 +++ b/src/ZF/arith_data.ML	Thu Oct 30 16:55:29 2014 +0100
    18.3 @@ -51,7 +51,7 @@
    18.4  
    18.5  (*Apply the given rewrite (if present) just once*)
    18.6  fun gen_trans_tac th2 NONE      = all_tac
    18.7 -  | gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2));
    18.8 +  | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve_tac [th RS th2]);
    18.9  
   18.10  (*Use <-> or = depending on the type of t*)
   18.11  fun mk_eq_iff(t,u) =