--- a/src/Pure/Isar/class.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/class.ML Thu Oct 30 16:20:46 2014 +0100
@@ -434,7 +434,7 @@
(fst o rules thy) sub];
val classrel =
Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
- (K (EVERY (map (TRYALL o rtac) intros)));
+ (K (EVERY (map (TRYALL o resolve_tac o single) intros)));
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
--- a/src/Pure/Isar/class_declaration.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/class_declaration.ML Thu Oct 30 16:20:46 2014 +0100
@@ -56,7 +56,7 @@
val loc_intro_tac =
(case Locale.intros_of thy class of
(_, NONE) => all_tac
- | (_, SOME intro) => ALLGOALS (rtac intro));
+ | (_, SOME intro) => ALLGOALS (resolve_tac [intro]));
val tac = loc_intro_tac
THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
in Element.prove_witness empty_ctxt prop tac end) some_prop;
--- a/src/Pure/Isar/element.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/element.ML Thu Oct 30 16:20:46 2014 +0100
@@ -258,14 +258,15 @@
fun prove_witness ctxt t tac =
Witness (t,
Thm.close_derivation
- (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
+ (Goal.prove ctxt [] [] (mark_witness t)
+ (fn _ => resolve_tac [Drule.protectI] 1 THEN tac)));
local
val refine_witness =
Proof.refine (Method.Basic (K (NO_CASES o
- K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI)))))))));
+ K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac [Drule.protectI])))))))));
fun gen_witness_proof proof after_qed wit_propss eq_props =
let
--- a/src/Pure/Isar/method.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/method.ML Thu Oct 30 16:20:46 2014 +0100
@@ -100,7 +100,7 @@
local
fun cut_rule_tac rule =
- rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
+ resolve_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
in
@@ -147,7 +147,7 @@
(* this -- resolve facts directly *)
-val this = METHOD (EVERY o map (HEADGOAL o rtac));
+val this = METHOD (EVERY o map (HEADGOAL o resolve_tac o single));
(* fact -- composition by facts from context *)
@@ -162,7 +162,7 @@
fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
if cond (Logic.strip_assums_concl prop)
- then rtac rule i else no_tac);
+ then resolve_tac [rule] i else no_tac);
in
--- a/src/Pure/Isar/proof.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/proof.ML Thu Oct 30 16:20:46 2014 +0100
@@ -442,12 +442,12 @@
Goal.norm_hhf_tac ctxt THEN'
SUBGOAL (fn (goal, i) =>
if can Logic.unprotect (Logic.strip_assums_concl goal) then
- etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
+ eresolve_tac [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
else finish_tac ctxt (n - 1) (i + 1));
fun goal_tac ctxt rule =
Goal.norm_hhf_tac ctxt THEN'
- rtac rule THEN'
+ resolve_tac [rule] THEN'
finish_tac ctxt (Thm.nprems_of rule);
fun FINDGOAL tac st =
@@ -886,7 +886,7 @@
fun refine_terms n =
refine (Method.Basic (K (NO_CASES o
K (HEADGOAL (PRECISE_CONJUNCTS n
- (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))
+ (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac [Drule.termI])))))))))
#> Seq.hd;
in
--- a/src/Pure/Tools/find_theorems.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Thu Oct 30 16:20:46 2014 +0100
@@ -206,9 +206,10 @@
val goal' = Thm.transfer thy' goal;
fun limited_etac thm i =
- Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o etac thm i;
+ Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
+ eresolve_tac [thm] i;
fun try_thm thm =
- if Thm.no_prems thm then rtac thm 1 goal'
+ if Thm.no_prems thm then resolve_tac [thm] 1 goal'
else
(limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
1 goal';
--- a/src/Pure/goal.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/goal.ML Thu Oct 30 16:20:46 2014 +0100
@@ -293,7 +293,7 @@
val adhoc_conjunction_tac = REPEAT_ALL_NEW
(SUBGOAL (fn (goal, i) =>
- if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
+ if can Logic.dest_conjunction goal then resolve_tac [Conjunction.conjunctionI] i
else no_tac));
val conjunction_tac = SUBGOAL (fn (goal, i) =>
@@ -317,7 +317,7 @@
(* hhf normal form *)
fun norm_hhf_tac ctxt =
- rtac Drule.asm_rl (*cheap approximation -- thanks to builtin Logic.flatten_params*)
+ resolve_tac [Drule.asm_rl] (*cheap approximation -- thanks to builtin Logic.flatten_params*)
THEN' SUBGOAL (fn (t, i) =>
if Drule.is_norm_hhf t then all_tac
else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
@@ -335,7 +335,7 @@
val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
val tacs = Rs |> map (fn R =>
- etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
+ eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac);
in fold_rev (curry op APPEND') tacs (K no_tac) i end);
end;
--- a/src/Pure/skip_proof.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/skip_proof.ML Thu Oct 30 16:20:46 2014 +0100
@@ -38,6 +38,6 @@
(* cheat_tac *)
fun cheat_tac i st =
- rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
+ resolve_tac [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
end;
--- a/src/Pure/tactic.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/tactic.ML Thu Oct 30 16:20:46 2014 +0100
@@ -181,7 +181,7 @@
(*The conclusion of the rule gets assumed in subgoal i,
while subgoal i+1,... are the premises of the rule.*)
-fun cut_tac rule i = rtac cut_rl i THEN rtac rule (i + 1);
+fun cut_tac rule i = resolve_tac [cut_rl] i THEN resolve_tac [rule] (i + 1);
(*"Cut" a list of rules into the goal. Their premises will become new
subgoals.*)
@@ -327,7 +327,7 @@
| Then (SOME tac) tac' = SOME(tac THEN' tac');
fun thins H (tac,n) =
if p H then (tac,n+1)
- else (Then tac (rotate_tac n THEN' etac thin_rl),0);
+ else (Then tac (rotate_tac n THEN' eresolve_tac [thin_rl]),0);
in SUBGOAL(fn (subg,n) =>
let val Hs = Logic.strip_assums_hyp subg
in case fst(fold thins Hs (NONE,0)) of
--- a/src/Pure/thm.ML Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/thm.ML Thu Oct 30 16:20:46 2014 +0100
@@ -1390,7 +1390,7 @@
(*Rotates a rule's premises to the left by k, leaving the first j premises
unchanged. Does nothing if k=0 or if k equals n-j, where n is the
- number of premises. Useful with etac and underlies defer_tac*)
+ number of premises. Useful with eresolve_tac and underlies defer_tac*)
fun permute_prems j k rl =
let
val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = rl;