--- 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
--- 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 =
--- 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
--- 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
--- 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
--- 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;
--- 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 *)
--- 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) =
--- 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
--- 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 =
--- 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;
--- 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;
--- 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);
--- 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
--- 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};
--- 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
--- 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))));
--- 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) =