--- a/src/CCL/CCL.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/CCL/CCL.thy Tue Feb 10 16:46:21 2015 +0100
@@ -204,7 +204,8 @@
fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
val inj_lemmas = maps mk_inj_lemmas rews
in
- CHANGED (REPEAT (ares_tac [@{thm iffI}, @{thm allI}, @{thm conjI}] i ORELSE
+ CHANGED (REPEAT (assume_tac ctxt i ORELSE
+ resolve_tac ctxt @{thms iffI allI conjI} i ORELSE
eresolve_tac ctxt inj_lemmas i ORELSE
asm_simp_tac (ctxt addsimps rews) i))
end;
--- a/src/CCL/Type.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/CCL/Type.thy Tue Feb 10 16:46:21 2015 +0100
@@ -127,9 +127,10 @@
fun mk_ncanT_tac top_crls crls =
SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
resolve_tac ctxt ([major] RL top_crls) 1 THEN
- REPEAT_SOME (eresolve_tac ctxt (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
+ REPEAT_SOME (eresolve_tac ctxt (crls @ @{thms exE bexE conjE disjE})) THEN
ALLGOALS (asm_simp_tac ctxt) THEN
- ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
+ ALLGOALS (assume_tac ctxt ORELSE' resolve_tac ctxt (prems RL [@{thm lem}])
+ ORELSE' eresolve_tac ctxt @{thms bspec}) THEN
safe_tac (ctxt addSIs prems))
*}
--- a/src/CCL/Wfd.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/CCL/Wfd.thy Tue Feb 10 16:46:21 2015 +0100
@@ -451,10 +451,11 @@
THEN eresolve_tac ctxt @{thms rcall_lemmas} i
fun raw_step_tac ctxt prems i =
- ares_tac (prems@type_rls) i ORELSE
+ assume_tac ctxt i ORELSE
+ resolve_tac ctxt (prems @ type_rls) i ORELSE
rcall_tac ctxt i ORELSE
- ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
- match_tac ctxt [@{thm SubtypeI}] i
+ ematch_tac ctxt @{thms SubtypeE} i ORELSE
+ match_tac ctxt @{thms SubtypeI} i
fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
--- a/src/Cube/Example.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/Cube/Example.thy Tue Feb 10 16:46:21 2015 +0100
@@ -10,17 +10,17 @@
J. Functional Programming.\<close>
method_setup depth_solve =
- \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
- (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
+ \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
+ (DEPTH_SOLVE (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
method_setup depth_solve1 =
- \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
- (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
+ \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
+ (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
method_setup strip_asms =
\<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN
- DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))\<close>
+ DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close>
subsection \<open>Simple types\<close>
--- a/src/HOL/HOL.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/HOL.thy Tue Feb 10 16:46:21 2015 +0100
@@ -904,7 +904,8 @@
shows R
apply (rule ex1E [OF major])
apply (rule prem)
-apply (tactic {* ares_tac @{thms allI} 1 *})+
+apply assumption
+apply (rule allI)+
apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
apply iprover
done
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Feb 10 16:46:21 2015 +0100
@@ -1061,7 +1061,8 @@
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
- DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
+ DEPTH_SOLVE_1
+ (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
(prems ~~ constr_defs))]);
val case_names_induct = Old_Datatype_Data.mk_case_names_induct descr'';
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Tue Feb 10 16:46:21 2015 +0100
@@ -538,7 +538,7 @@
method_setup valid_certificate_tac = {*
Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
(fn i =>
- EVERY [ftac @{thm Gets_certificate_valid} i,
+ EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
assume_tac ctxt i,
etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
*}
--- a/src/HOL/SET_Protocol/Purchase.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy Tue Feb 10 16:46:21 2015 +0100
@@ -482,7 +482,7 @@
method_setup valid_certificate_tac = {*
Args.goal_spec >> (fn quant =>
fn ctxt => SIMPLE_METHOD'' quant (fn i =>
- EVERY [ftac @{thm Gets_certificate_valid} i,
+ EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)]))
*}
--- a/src/HOL/Set.thy Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Set.thy Tue Feb 10 16:46:21 2015 +0100
@@ -75,7 +75,7 @@
resolve_tac ctxt @{thms iffI} 1 THEN
ALLGOALS
(EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
- DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
+ DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
*}
lemmas CollectE = CollectD [elim_format]
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 10 16:46:21 2015 +0100
@@ -94,7 +94,7 @@
REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
- (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
+ (EVERY' [rtac notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
REPEAT_DETERM o FIRST'
[EVERY' [rtac @{thm subset_emptyI}, eresolve_tac ctxt wits],
EVERY' [rtac subsetI, rtac FalseE, eresolve_tac ctxt wits],
--- a/src/HOL/Tools/inductive.ML Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Feb 10 16:46:21 2015 +0100
@@ -452,7 +452,8 @@
REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules1)),
REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules2)),
EVERY (map (fn prem =>
- DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
+ DEPTH_SOLVE_1 (assume_tac ctxt4 1 ORELSE
+ resolve_tac ctxt [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
(tl prems))])
|> singleton (Proof_Context.export ctxt'' ctxt'''),
map #2 c_intrs, length Ts)
@@ -746,9 +747,11 @@
REPEAT (FIRSTGOAL
(resolve_tac ctxt3 [conjI, impI] ORELSE'
(eresolve_tac ctxt3 [notE] THEN' assume_tac ctxt3))),
- EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
- (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
- conjI, refl] 1)) prems)]);
+ EVERY (map (fn prem =>
+ DEPTH_SOLVE_1 (assume_tac ctxt3 1 ORELSE
+ resolve_tac ctxt3
+ [rewrite_rule ctxt3 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
+ conjI, refl] 1)) prems)]);
val lemma = Goal.prove_sorry ctxt'' [] []
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
--- a/src/HOL/Tools/simpdata.ML Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Tools/simpdata.ML Tue Feb 10 16:46:21 2015 +0100
@@ -73,8 +73,10 @@
(mk_simp_implies @{prop "(x::'a) = y"})
(fn {context = ctxt, prems} => EVERY
[rewrite_goals_tac ctxt @{thms simp_implies_def},
- REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
- map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
+ REPEAT (assume_tac ctxt 1 ORELSE
+ resolve_tac ctxt
+ (@{thm meta_eq_to_obj_eq} ::
+ map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
end
end;