# HG changeset patch # User wenzelm # Date 1414684529 -3600 # Node ID 59203adfc33f8f9095af0fbbe18488a6c8e658b8 # Parent e84d900cd287a0f914199ae36af3b3676621d57b eliminated aliases; diff -r e84d900cd287 -r 59203adfc33f src/FOL/ex/Miniscope.thy --- a/src/FOL/ex/Miniscope.thy Thu Oct 30 16:20:46 2014 +0100 +++ b/src/FOL/ex/Miniscope.thy Thu Oct 30 16:55:29 2014 +0100 @@ -65,7 +65,7 @@ ML {* val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps}); -fun mini_tac ctxt = rtac @{thm ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt); +fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt); *} end diff -r e84d900cd287 -r 59203adfc33f src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/FOL/simpdata.ML Thu Oct 30 16:55:29 2014 +0100 @@ -107,7 +107,9 @@ val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; fun unsafe_solver ctxt = - FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), atac, etac @{thm FalseE}]; + FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), + assume_tac, + eresolve_tac @{thms FalseE}]; (*No premature instantiation of variables during simplification*) fun safe_solver ctxt = diff -r e84d900cd287 -r 59203adfc33f src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/Arith/cancel_numerals.ML Thu Oct 30 16:55:29 2014 +0100 @@ -92,12 +92,12 @@ Option.map (export o Data.simplify_meta_eq ctxt) (if n2 <= n1 then Data.prove_conv - [Data.trans_tac reshape, rtac Data.bal_add1 1, + [Data.trans_tac reshape, resolve_tac [Data.bal_add1] 1, Data.numeral_simp_tac ctxt] ctxt prems (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2')) else Data.prove_conv - [Data.trans_tac reshape, rtac Data.bal_add2 1, + [Data.trans_tac reshape, resolve_tac [Data.bal_add2] 1, Data.numeral_simp_tac ctxt] ctxt prems (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2')))) end diff -r e84d900cd287 -r 59203adfc33f src/Provers/Arith/combine_numerals.ML --- a/src/Provers/Arith/combine_numerals.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/Arith/combine_numerals.ML Thu Oct 30 16:55:29 2014 +0100 @@ -83,7 +83,7 @@ in Option.map (export o Data.simplify_meta_eq ctxt) (Data.prove_conv - [Data.trans_tac reshape, rtac Data.left_distrib 1, + [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1, Data.numeral_simp_tac ctxt] ctxt (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) end diff -r e84d900cd287 -r 59203adfc33f src/Provers/blast.ML --- a/src/Provers/blast.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/blast.ML Thu Oct 30 16:55:29 2014 +0100 @@ -488,8 +488,8 @@ (*Resolution/matching tactics: if upd then the proof state may be updated. Matching makes the tactics more deterministic in the presence of Vars.*) -fun emtac ctxt upd rl = TRACE ctxt rl (if upd then etac rl else ematch_tac [rl]); -fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then rtac rl else match_tac [rl]); +fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]); +fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]); (*Tableau rule from elimination rule. Flag "upd" says that the inference updated the branch. @@ -624,7 +624,7 @@ (*Tactic. Convert *Goal* to negated assumption in FIRST position*) fun negOfGoal_tac ctxt i = - TRACE ctxt Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i; + TRACE ctxt Data.ccontr (resolve_tac [Data.ccontr]) i THEN rotate_tac ~1 i; fun traceTerm ctxt t = let val thy = Proof_Context.theory_of ctxt diff -r e84d900cd287 -r 59203adfc33f src/Provers/classical.ML --- a/src/Provers/classical.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/classical.ML Thu Oct 30 16:55:29 2014 +0100 @@ -157,7 +157,7 @@ val rule'' = rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => if i = 1 orelse redundant_hyp goal - then etac thin_rl i + then eresolve_tac [thin_rl] i else all_tac)) |> Seq.hd |> Drule.zero_var_indexes; @@ -209,7 +209,7 @@ let val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl); - in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; + in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end; (**** Classical rule sets ****) @@ -689,8 +689,8 @@ fun ctxt addafter (name, tac2) = ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt); -fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dtac thm THEN' assume_tac); -fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => etac thm THEN' assume_tac); +fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac); +fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac); fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac); fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac); @@ -909,7 +909,7 @@ val ruleq = Drule.multi_resolves facts rules; val _ = Method.trace ctxt rules; in - fn st => Seq.maps (fn rule => rtac rule i st) ruleq + fn st => Seq.maps (fn rule => resolve_tac [rule] i st) ruleq end) THEN_ALL_NEW Goal.norm_hhf_tac ctxt; diff -r e84d900cd287 -r 59203adfc33f src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/hypsubst.ML Thu Oct 30 16:55:29 2014 +0100 @@ -126,7 +126,7 @@ val (k, _) = eq_var false false false t val ok = (eq_var false false true t |> fst) > k handle EQ_VAR => true - in if ok then EVERY [rotate_tac k i, etac thin_rl i, rotate_tac (~k) i] + in if ok then EVERY [rotate_tac k i, eresolve_tac [thin_rl] i, rotate_tac (~k) i] else no_tac end handle EQ_VAR => no_tac) @@ -151,11 +151,11 @@ val (k, (orient, is_free)) = eq_var bnd true true Bi val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd)) in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i, - if not is_free then etac thin_rl i - else if orient then etac Data.rev_mp i - else etac (Data.sym RS Data.rev_mp) i, + if not is_free then eresolve_tac [thin_rl] i + else if orient then eresolve_tac [Data.rev_mp] i + else eresolve_tac [Data.sym RS Data.rev_mp] i, rotate_tac (~k) i, - if is_free then rtac Data.imp_intr i else all_tac] + if is_free then resolve_tac [Data.imp_intr] i else all_tac] end handle THM _ => no_tac | EQ_VAR => no_tac) end; @@ -194,7 +194,7 @@ end | NONE => no_tac); -val imp_intr_tac = rtac Data.imp_intr; +val imp_intr_tac = resolve_tac [Data.imp_intr]; fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; val dup_subst = rev_dup_elim ssubst @@ -211,9 +211,9 @@ val rl = if orient then rl else Data.sym RS rl in DETERM - (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), + (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i), rotate_tac 1 i, - REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), + REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i), inst_subst_tac orient rl i, REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) end @@ -245,7 +245,7 @@ fun reverse_n_tac 0 i = all_tac | reverse_n_tac 1 i = rotate_tac ~1 i | reverse_n_tac n i = - REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN + REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac [Data.rev_mp] i) THEN REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i); (*Use imp_intr, comparing the old hyps with the new ones as they come out.*) @@ -279,9 +279,9 @@ in if trace then tracing "Substituting an equality" else (); DETERM - (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), + (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i), rotate_tac 1 i, - REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), + REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i), inst_subst_tac symopt (if symopt then ssubst else Data.subst) i, all_imp_intr_tac hyps i]) end @@ -291,7 +291,7 @@ fails unless the substitution has an effect*) fun stac th = let val th' = th RS Data.rev_eq_reflection handle THM _ => th - in CHANGED_GOAL (rtac (th' RS ssubst)) end; + in CHANGED_GOAL (resolve_tac [th' RS ssubst]) end; (* method setup *) diff -r e84d900cd287 -r 59203adfc33f src/Provers/quantifier1.ML --- a/src/Provers/quantifier1.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/quantifier1.ML Thu Oct 30 16:55:29 2014 +0100 @@ -126,10 +126,10 @@ yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt; val thm = Goal.prove ctxt' [] [] goal - (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt''); + (fn {context = ctxt'', ...} => resolve_tac [Data.iff_reflection] 1 THEN tac ctxt''); in singleton (Variable.export ctxt' ctxt) thm end; -fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i); +fun qcomm_tac qcomm qI i = REPEAT_DETERM (resolve_tac [qcomm] i THEN resolve_tac [qI] i); (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) Better: instantiate exI @@ -138,9 +138,10 @@ val excomm = Data.ex_comm RS Data.iff_trans; in val prove_one_point_ex_tac = - qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN + qcomm_tac excomm Data.iff_exI 1 THEN resolve_tac [Data.iffI] 1 THEN ALLGOALS - (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI, + (EVERY' [eresolve_tac [Data.exE], REPEAT_DETERM o eresolve_tac [Data.conjE], + resolve_tac [Data.exI], DEPTH_SOLVE_1 o ares_tac [Data.conjI]]) end; @@ -150,12 +151,17 @@ local val tac = SELECT_GOAL - (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp, - REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]); + (EVERY1 [REPEAT o dresolve_tac [Data.uncurry], + REPEAT o resolve_tac [Data.impI], + eresolve_tac [Data.mp], + REPEAT o eresolve_tac [Data.conjE], + REPEAT o ares_tac [Data.conjI]]); val allcomm = Data.all_comm RS Data.iff_trans; in val prove_one_point_all_tac = - EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac]; + EVERY1 [qcomm_tac allcomm Data.iff_allI, + resolve_tac [Data.iff_allI], + resolve_tac [Data.iffI], tac, tac]; end fun renumber l u (Bound i) = diff -r e84d900cd287 -r 59203adfc33f src/Provers/splitter.ML --- a/src/Provers/splitter.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/splitter.ML Thu Oct 30 16:55:29 2014 +0100 @@ -99,7 +99,7 @@ val lift = Goal.prove_global Pure.thy ["P", "Q", "R"] [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"] (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))") - (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1) + (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN resolve_tac [reflexive_thm] 1) val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift; @@ -365,11 +365,11 @@ (case apsns of [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state | p::_ => EVERY [lift_tac Ts t p, - rtac reflexive_thm (i+1), + resolve_tac [reflexive_thm] (i+1), lift_split_tac] state) end in COND (has_fewer_prems i) no_tac - (rtac meta_iffD i THEN lift_split_tac) + (resolve_tac [meta_iffD] i THEN lift_split_tac) end; in (split_tac, exported_split_posns) end; (* mk_case_split_tac *) @@ -400,16 +400,16 @@ (* does not work properly if the split variable is bound by a quantifier *) fun flat_prems_tac i = SUBGOAL (fn (t,i) => (if first_prem_is_disj t - then EVERY[etac Data.disjE i,rotate_tac ~1 i, + then EVERY[eresolve_tac [Data.disjE] i, rotate_tac ~1 i, rotate_tac ~1 (i+1), flat_prems_tac (i+1)] else all_tac) THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i) THEN REPEAT (dresolve_tac [Data.notnotD] i)) i; in if n<0 then no_tac else (DETERM (EVERY' - [rotate_tac n, etac Data.contrapos2, + [rotate_tac n, eresolve_tac [Data.contrapos2], split_tac splits, - rotate_tac ~1, etac Data.contrapos, rotate_tac ~1, + rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1, flat_prems_tac] i)) end; in SUBGOAL tac diff -r e84d900cd287 -r 59203adfc33f src/Tools/case_product.ML --- a/src/Tools/case_product.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Tools/case_product.ML Thu Oct 30 16:55:29 2014 +0100 @@ -70,9 +70,9 @@ val (p_cons1 :: p_cons2 :: premss) = unflat struc prems val thm2' = thm2 OF p_cons2 in - rtac (thm1 OF p_cons1) + resolve_tac [thm1 OF p_cons1] THEN' EVERY' (map (fn p => - rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss) + resolve_tac [thm2'] THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss) end fun combine ctxt thm1 thm2 = diff -r e84d900cd287 -r 59203adfc33f src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Tools/eqsubst.ML Thu Oct 30 16:55:29 2014 +0100 @@ -250,7 +250,7 @@ RW_Inst.rw ctxt m rule conclthm |> unfix_frees cfvs |> Conv.fconv_rule Drule.beta_eta_conversion - |> (fn r => rtac r i st); + |> (fn r => resolve_tac [r] i st); (* substitute within the conclusion of goal i of gth, using a meta equation rule. Note that we assume rule has var indicies zero'd *) @@ -332,7 +332,7 @@ |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *) in (* ~j because new asm starts at back, thus we subtract 1 *) - Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2) + Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dresolve_tac [preelimrule] i st2) end; diff -r e84d900cd287 -r 59203adfc33f src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Tools/induct.ML Thu Oct 30 16:55:29 2014 +0100 @@ -512,7 +512,7 @@ in CASES (Rule_Cases.make_common (thy, Thm.prop_of (Rule_Cases.internalize_params rule')) cases) - ((Method.insert_tac more_facts THEN' rtac rule' THEN_ALL_NEW + ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW (if simp then TRY o trivial_tac else K all_tac)) i) st end) end; @@ -683,7 +683,8 @@ in (case goal_concl n [] goal of SOME concl => - (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i + (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' + resolve_tac [asm_rl]) i | NONE => all_tac) end); @@ -804,7 +805,7 @@ |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking)) |> Seq.maps (fn rule' => CASES (rule_cases ctxt rule' cases) - (rtac rule' i THEN + (resolve_tac [rule'] i THEN PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))) end) THEN_ALL_NEW_CASES @@ -862,7 +863,7 @@ |> Seq.maps (fn rule' => CASES (Rule_Cases.make_common (thy, Thm.prop_of (Rule_Cases.internalize_params rule')) cases) - (Method.insert_tac more_facts i THEN rtac rule' i) st)) + (Method.insert_tac more_facts i THEN resolve_tac [rule'] i) st)) end); end; diff -r e84d900cd287 -r 59203adfc33f src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Thu Oct 30 16:20:46 2014 +0100 +++ b/src/ZF/Datatype_ZF.thy Thu Oct 30 16:55:29 2014 +0100 @@ -95,7 +95,7 @@ else (); val goal = Logic.mk_equals (old, new) val thm = Goal.prove ctxt [] [] goal - (fn _ => rtac @{thm iff_reflection} 1 THEN + (fn _ => resolve_tac @{thms iff_reflection} 1 THEN simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1) handle ERROR msg => (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal); diff -r e84d900cd287 -r 59203adfc33f src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/ZF/Tools/datatype_package.ML Thu Oct 30 16:55:29 2014 +0100 @@ -289,7 +289,7 @@ (*Proves a single case equation. Could use simp_tac, but it's slower!*) (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt [con_def], - rtac case_trans 1, + resolve_tac [case_trans] 1, REPEAT (resolve_tac [@{thm refl}, split_trans, Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]); @@ -330,7 +330,7 @@ (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg)) (*Proves a single recursor equation.*) (fn {context = ctxt, ...} => EVERY - [rtac recursor_trans 1, + [resolve_tac [recursor_trans] 1, simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1, IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]); in diff -r e84d900cd287 -r 59203adfc33f src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/ZF/Tools/inductive_package.ML Thu Oct 30 16:55:29 2014 +0100 @@ -189,7 +189,7 @@ val bnd_mono = Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)) (fn _ => EVERY - [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1, + [resolve_tac [@{thm Collect_subset} RS @{thm bnd_monoI}] 1, REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]); val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs); @@ -218,13 +218,13 @@ [DETERM (stac unfold 1), REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1), (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*) - rtac disjIn 2, + resolve_tac [disjIn] 2, (*Not ares_tac, since refl must be tried before equality assumptions; backtracking may occur if the premises have extra variables!*) DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2), (*Now solve the equations like Tcons(a,f) = Inl(?b4)*) rewrite_goals_tac ctxt con_defs, - REPEAT (rtac @{thm refl} 2), + REPEAT (resolve_tac @{thms refl} 2), (*Typechecking; this can fail*) if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:" else all_tac, @@ -332,15 +332,15 @@ setSolver (mk_solver "minimal" (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt) ORELSE' assume_tac - ORELSE' etac @{thm FalseE})); + ORELSE' eresolve_tac @{thms FalseE})); val quant_induct = Goal.prove_global thy1 [] ind_prems (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred))) (fn {context = ctxt, prems} => EVERY [rewrite_goals_tac ctxt part_rec_defs, - rtac (@{thm impI} RS @{thm allI}) 1, - DETERM (etac raw_induct 1), + resolve_tac [@{thm impI} RS @{thm allI}] 1, + DETERM (eresolve_tac [raw_induct] 1), (*Push Part inside Collect*) full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1, (*This CollectE and disjE separates out the introduction rules*) @@ -470,8 +470,8 @@ (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1 THEN (*unpackage and use "prem" in the corresponding place*) - REPEAT (rtac @{thm impI} 1) THEN - rtac (rewrite_rule ctxt all_defs prem) 1 THEN + REPEAT (resolve_tac @{thms impI} 1) THEN + resolve_tac [rewrite_rule ctxt all_defs prem] 1 THEN (*prem must not be REPEATed below: could loop!*) DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE' eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos)))) @@ -483,7 +483,7 @@ Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms) mutual_induct_concl (fn {context = ctxt, prems} => EVERY - [rtac (quant_induct RS lemma) 1, + [resolve_tac [quant_induct RS lemma] 1, mutual_ind_tac ctxt (rev prems) (length prems)]) else @{thm TrueI}; diff -r e84d900cd287 -r 59203adfc33f src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/ZF/Tools/primrec_package.ML Thu Oct 30 16:55:29 2014 +0100 @@ -176,7 +176,8 @@ val eqn_thms = eqn_terms |> map (fn t => Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) - (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1])); + (fn {context = ctxt, ...} => + EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac @{thms refl} 1])); val (eqn_thms', thy2) = thy1 diff -r e84d900cd287 -r 59203adfc33f src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/ZF/Tools/typechk.ML Thu Oct 30 16:55:29 2014 +0100 @@ -99,7 +99,7 @@ (*Instantiates variables in typing conditions. drawback: does not simplify conjunctions*) fun type_solver_tac ctxt hyps = SELECT_GOAL - (DEPTH_SOLVE (etac @{thm FalseE} 1 + (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1 ORELSE basic_res_tac 1 ORELSE (ares_tac hyps 1 APPEND typecheck_step_tac (tcset_of ctxt)))); diff -r e84d900cd287 -r 59203adfc33f src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/ZF/arith_data.ML Thu Oct 30 16:55:29 2014 +0100 @@ -51,7 +51,7 @@ (*Apply the given rewrite (if present) just once*) fun gen_trans_tac th2 NONE = all_tac - | gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2)); + | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve_tac [th RS th2]); (*Use <-> or = depending on the type of t*) fun mk_eq_iff(t,u) =