--- a/src/HOL/HOLCF/Tools/cpodef.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sat Jul 27 16:35:51 2013 +0200
@@ -73,7 +73,7 @@
val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
- val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
+ val tac = rtac (@{thm typedef_cpo} OF cpo_thms) 1
val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
(* transfer thms so that they will know about the new cpo instance *)
val cpo_thms' = map (Thm.transfer thy) cpo_thms
@@ -112,7 +112,7 @@
val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
- val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
+ val tac = rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
val pcpo_thms' = map (Thm.transfer thy) pcpo_thms
fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms')
@@ -184,7 +184,7 @@
val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
val thy = lthy
|> Class.prove_instantiation_exit
- (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
+ (K (rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
in ((info, below_def), thy) end
fun prepare_cpodef
@@ -207,7 +207,7 @@
fun cpodef_result nonempty admissible thy =
let
val ((info as (_, {type_definition, ...}), below_def), thy) = thy
- |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1)
+ |> add_podef typ set opt_morphs (rtac nonempty 1)
val (cpo_info, thy) = thy
|> prove_cpo name newT morphs type_definition below_def admissible
in
@@ -239,7 +239,7 @@
fun pcpodef_result bottom_mem admissible thy =
let
- val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
+ val tac = rtac exI 1 THEN rtac bottom_mem 1
val ((info as (_, {type_definition, ...}), below_def), thy) = thy
|> add_podef typ set opt_morphs tac
val (cpo_info, thy) = thy
--- a/src/HOL/HOLCF/Tools/domaindef.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sat Jul 27 16:35:51 2013 +0200
@@ -167,7 +167,7 @@
liftemb_def, liftprj_def, liftdefl_def]
val thy = lthy
|> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
+ (K (rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
|> Local_Theory.exit_global
(*other theorems*)
--- a/src/HOL/Nominal/nominal_induct.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Sat Jul 27 16:35:51 2013 +0200
@@ -124,7 +124,7 @@
(finish_rule (Induct.internalize more_consumes rule)) i st'
|> Seq.maps (fn rule' =>
CASES (rule_cases ctxt rule' cases)
- (Tactic.rtac (rename_params_rule false [] rule') i THEN
+ (rtac (rename_params_rule false [] rule') i THEN
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
THEN_ALL_NEW_CASES
((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
--- a/src/HOL/SMT_Examples/boogie.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML Sat Jul 27 16:35:51 2013 +0200
@@ -18,7 +18,7 @@
val isabelle_name =
- let
+ let
fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else
(case s of
"." => "_o_"
@@ -303,7 +303,7 @@
let
val (text, thy') = Thy_Load.use_file (Path.explode file_name) thy
val lines = explode_lines text
-
+
val ((axioms, vc), ctxt) =
empty_context
|> parse_lines lines
@@ -312,7 +312,7 @@
val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
boogie_tac context prems)
- val _ = Output.writeln "Verification condition proved successfully"
+ val _ = writeln "Verification condition proved successfully"
in thy' end
--- a/src/HOL/Tools/Function/termination.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Function/termination.ML Sat Jul 27 16:35:51 2013 +0200
@@ -305,7 +305,7 @@
in
(PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
- THEN Raw_Simplifier.rewrite_goal_tac Un_aci_simps 1) st (* eliminate duplicates *)
+ THEN rewrite_goal_tac Un_aci_simps 1) st (* eliminate duplicates *)
end
end
--- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sat Jul 27 16:35:51 2013 +0200
@@ -105,7 +105,7 @@
so that "Thm.equal_elim" works below. *)
val t0 $ _ $ t2 = prop_of eq_th
val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
- val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
+ val eq_th' = Goal.prove_internal [] eq_ct (K (rtac eq_th 1))
in Thm.equal_elim eq_th' th end
fun clause_params ordering =
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Jul 27 16:35:51 2013 +0200
@@ -236,7 +236,7 @@
(PEEK nprems_of
(fn n =>
ALLGOALS (fn i =>
- Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i
+ rewrite_goal_tac [@{thm split_paired_all}] i
THEN (SUBPROOF (instantiate i n) ctxt i))))
in
Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sat Jul 27 16:35:51 2013 +0200
@@ -83,8 +83,7 @@
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- Simplifier.rewrite_goal_tac
- (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end) ctxt 1
| Abs _ => raise Fail "prove_param: No valid parameter term"
in
@@ -169,7 +168,7 @@
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- Simplifier.rewrite_goal_tac
+ rewrite_goal_tac
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end
THEN REPEAT_DETERM (rtac @{thm refl} 1))
@@ -210,8 +209,7 @@
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- Simplifier.rewrite_goal_tac
- (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end) ctxt 1
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
| prove_prems out_ts ((p, deriv) :: ps) =
--- a/src/HOL/Tools/SMT/smt_solver.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sat Jul 27 16:35:51 2013 +0200
@@ -354,12 +354,12 @@
fun tag_rules thms = map_index (apsnd (pair NONE)) thms
fun tag_prems thms = map (pair ~1 o pair NONE) thms
- fun resolve (SOME thm) = Tactic.rtac thm 1
+ fun resolve (SOME thm) = rtac thm 1
| resolve NONE = no_tac
fun tac prove ctxt rules =
CONVERSION (SMT_Normalize.atomize_conv ctxt)
- THEN' Tactic.rtac @{thm ccontr}
+ THEN' rtac @{thm ccontr}
THEN' SUBPROOF (fn {context, prems, ...} =>
resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
in
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Sat Jul 27 16:35:51 2013 +0200
@@ -33,7 +33,7 @@
val prove_ite =
Z3_Proof_Tools.by_tac (
CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
- THEN' Tactic.rtac @{thm refl})
+ THEN' rtac @{thm refl})
@@ -71,7 +71,7 @@
val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
in
Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
- |> apply (Tactic.rtac @{thm injI})
+ |> apply (rtac @{thm injI})
|> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
|> Goal.norm_result o Goal.finish ctxt'
|> singleton (Variable.export ctxt' ctxt)
@@ -80,8 +80,8 @@
fun prove_rhs ctxt def lhs =
Z3_Proof_Tools.by_tac (
CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
- THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
- THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
+ THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
+ THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
fun expand thm ct =
@@ -142,7 +142,7 @@
fun prove_injectivity ctxt =
Z3_Proof_Tools.by_tac (
CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
- THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
+ THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
end
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Jul 27 16:35:51 2013 +0200
@@ -415,9 +415,9 @@
@{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
- Tactic.rtac thm ORELSE'
- (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
- (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
+ rtac thm ORELSE'
+ (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
+ (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
fun nnf_quant_tac_varified vars eq =
nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
@@ -557,7 +557,7 @@
val thm = meta_eq_of p
val rules' = Z3_Proof_Tools.varify vars thm :: rules
val cu = Z3_Proof_Tools.as_meta_eq ct
- val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
+ val tac = REPEAT_ALL_NEW (match_tac rules')
in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
end
@@ -580,10 +580,10 @@
val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
fun elim_unused_tac i st = (
- Tactic.match_tac [@{thm refl}]
- ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+ match_tac [@{thm refl}]
+ ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
ORELSE' (
- Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]
+ match_tac [@{thm iff_allI}, @{thm iff_exI}]
THEN' elim_unused_tac)) i st
in
@@ -603,8 +603,8 @@
val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
in
val quant_inst = Thm o Z3_Proof_Tools.by_tac (
- REPEAT_ALL_NEW (Tactic.match_tac [rule])
- THEN' Tactic.rtac @{thm excluded_middle})
+ REPEAT_ALL_NEW (match_tac [rule])
+ THEN' rtac @{thm excluded_middle})
end
@@ -639,10 +639,10 @@
apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
fun discharge_sk_tac i st = (
- Tactic.rtac @{thm trans} i
- THEN Tactic.resolve_tac sk_rules i
- THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
- THEN Tactic.rtac @{thm refl} i) st
+ rtac @{thm trans} i
+ THEN resolve_tac sk_rules i
+ THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+ THEN rtac @{thm refl} i) st
end
@@ -720,14 +720,14 @@
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
+ (rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
THEN_ALL_NEW (
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
+ (rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
THEN_ALL_NEW (
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
@@ -736,7 +736,7 @@
Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
(fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
+ (rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
THEN_ALL_NEW (
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
@@ -856,8 +856,7 @@
@{thm reflexive}, Z3_Proof_Literals.true_thm]
fun discharge_assms_tac rules =
- REPEAT (HEADGOAL (
- Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
+ REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
fun discharge_assms rules thm =
if Thm.nprems_of thm = 0 then Goal.norm_result thm
--- a/src/HOL/Tools/inductive.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/inductive.ML Sat Jul 27 16:35:51 2013 +0200
@@ -533,7 +533,7 @@
val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
(fn _ => assume_tac 1);
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
-val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
+val elim_tac = REPEAT o eresolve_tac elim_rls;
fun simp_case_tac ctxt i =
EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
--- a/src/Provers/classical.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Provers/classical.ML Sat Jul 27 16:35:51 2013 +0200
@@ -158,7 +158,7 @@
val rule'' =
rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
if i = 1 orelse redundant_hyp goal
- then Tactic.etac thin_rl i
+ then etac thin_rl i
else all_tac))
|> Seq.hd
|> Drule.zero_var_indexes;
@@ -897,9 +897,9 @@
val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
val rules = rules1 @ rules2 @ rules3 @ rules4;
val ruleq = Drule.multi_resolves facts rules;
+ val _ = Method.trace ctxt rules;
in
- Method.trace ctxt rules;
- fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
+ fn st => Seq.maps (fn rule => rtac rule i st) ruleq
end)
THEN_ALL_NEW Goal.norm_hhf_tac;
--- a/src/Pure/Isar/class.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/class.ML Sat Jul 27 16:35:51 2013 +0200
@@ -252,7 +252,7 @@
(fst o rules thy) sub];
val classrel =
Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
- (K (EVERY (map (TRYALL o Tactic.rtac) intros)));
+ (K (EVERY (map (TRYALL o rtac) 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 Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/class_declaration.ML Sat Jul 27 16:35:51 2013 +0200
@@ -56,7 +56,7 @@
val loc_intro_tac =
(case Locale.intros_of thy class of
(_, NONE) => all_tac
- | (_, SOME intro) => ALLGOALS (Tactic.rtac intro));
+ | (_, SOME intro) => ALLGOALS (rtac intro));
val tac = loc_intro_tac
THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
in Element.prove_witness empty_ctxt prop tac end) some_prop;
@@ -94,8 +94,8 @@
val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
val tac =
REPEAT (SOMEGOAL
- (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
- ORELSE' Tactic.assume_tac));
+ (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
+ ORELSE' assume_tac));
val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
--- a/src/Pure/Isar/element.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/element.ML Sat Jul 27 16:35:51 2013 +0200
@@ -262,17 +262,16 @@
fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
fun prove_witness ctxt t tac =
- Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
- Tactic.rtac Drule.protectI 1 THEN tac)));
+ Witness (t,
+ Thm.close_derivation
+ (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
local
val refine_witness =
Proof.refine (Method.Basic (K (RAW_METHOD
- (K (ALLGOALS
- (CONJUNCTS (ALLGOALS
- (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI))))))))));
+ (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI))))))))));
fun gen_witness_proof proof after_qed wit_propss eq_props =
let
--- a/src/Pure/Isar/expression.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/expression.ML Sat Jul 27 16:35:51 2013 +0200
@@ -666,17 +666,15 @@
val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
rewrite_goals_tac [pred_def] THEN
- Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
- Tactic.compose_tac (false,
- Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+ compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+ compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
val conjuncts =
(Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
|> Conjunction.elim_balanced (length ts);
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
Element.prove_witness defs_ctxt t
- (rewrite_goals_tac defs THEN
- Tactic.compose_tac (false, ax, 0) 1));
+ (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
in ((statement, intro, axioms), defs_thy) end;
in
--- a/src/Pure/Isar/method.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/method.ML Sat Jul 27 16:35:51 2013 +0200
@@ -108,7 +108,7 @@
local
fun cut_rule_tac rule =
- Tactic.rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
+ rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
in
@@ -135,8 +135,8 @@
(* unfold intro/elim rules *)
-fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
-fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
+fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
+fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
(* unfold/fold definitions *)
@@ -153,7 +153,7 @@
(* this -- resolve facts directly *)
-val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac));
+val this = METHOD (EVERY o map (HEADGOAL o rtac));
(* fact -- composition by facts from context *)
@@ -168,7 +168,7 @@
fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
if cond (Logic.strip_assums_concl prop)
- then Tactic.rtac rule i else no_tac);
+ then rtac rule i else no_tac);
in
@@ -215,7 +215,7 @@
THEN_ALL_NEW Goal.norm_hhf_tac;
fun gen_arule_tac tac j rules facts =
- EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);
+ EVERY' (gen_rule_tac tac rules facts :: replicate j assume_tac);
fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
let
@@ -229,14 +229,14 @@
in
-val rule_tac = gen_rule_tac Tactic.resolve_tac;
+val rule_tac = gen_rule_tac resolve_tac;
val rule = meth rule_tac;
val some_rule_tac = gen_some_rule_tac rule_tac;
val some_rule = meth' some_rule_tac;
-val erule = meth' (gen_arule_tac Tactic.eresolve_tac);
-val drule = meth' (gen_arule_tac Tactic.dresolve_tac);
-val frule = meth' (gen_arule_tac Tactic.forward_tac);
+val erule = meth' (gen_arule_tac eresolve_tac);
+val drule = meth' (gen_arule_tac dresolve_tac);
+val frule = meth' (gen_arule_tac forward_tac);
end;
@@ -461,10 +461,10 @@
setup (Binding.name "assumption") (Scan.succeed assumption)
"proof by assumption, preferring facts" #>
setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
- (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
+ (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
"rename parameters of goal" #>
setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
- (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
+ (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
"rotate assumptions of goal" #>
setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
"ML tactic as proof method" #>
--- a/src/Pure/Isar/proof.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/proof.ML Sat Jul 27 16:35:51 2013 +0200
@@ -446,12 +446,12 @@
Goal.norm_hhf_tac THEN'
SUBGOAL (fn (goal, i) =>
if can Logic.unprotect (Logic.strip_assums_concl goal) then
- Tactic.etac Drule.protectI i THEN finish_tac (n - 1) i
+ etac Drule.protectI i THEN finish_tac (n - 1) i
else finish_tac (n - 1) (i + 1));
fun goal_tac rule =
Goal.norm_hhf_tac THEN'
- Tactic.rtac rule THEN'
+ rtac rule THEN'
finish_tac (Thm.nprems_of rule);
fun FINDGOAL tac st =
--- a/src/Pure/Isar/rule_insts.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sat Jul 27 16:35:51 2013 +0200
@@ -332,11 +332,11 @@
[thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
| _ => error "Cannot have instantiations with multiple rules")));
-val res_inst_meth = method res_inst_tac (K Tactic.resolve_tac);
-val eres_inst_meth = method eres_inst_tac (K Tactic.eresolve_tac);
-val cut_inst_meth = method cut_inst_tac (K Tactic.cut_rules_tac);
-val dres_inst_meth = method dres_inst_tac (K Tactic.dresolve_tac);
-val forw_inst_meth = method forw_inst_tac (K Tactic.forward_tac);
+val res_inst_meth = method res_inst_tac (K resolve_tac);
+val eres_inst_meth = method eres_inst_tac (K eresolve_tac);
+val cut_inst_meth = method cut_inst_tac (K cut_rules_tac);
+val dres_inst_meth = method dres_inst_tac (K dresolve_tac);
+val forw_inst_meth = method forw_inst_tac (K forward_tac);
(* setup *)
--- a/src/Pure/goal.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/goal.ML Sat Jul 27 16:35:51 2013 +0200
@@ -425,7 +425,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 =>
- Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
+ etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
in fold_rev (curry op APPEND') tacs (K no_tac) i end);
--- a/src/Tools/case_product.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/case_product.ML Sat Jul 27 16:35:51 2013 +0200
@@ -70,10 +70,9 @@
val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
val thm2' = thm2 OF p_cons2
in
- Tactic.rtac (thm1 OF p_cons1)
+ rtac (thm1 OF p_cons1)
THEN' EVERY' (map (fn p =>
- Tactic.rtac thm2'
- THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
+ rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
end
fun combine ctxt thm1 thm2 =
--- a/src/Tools/eqsubst.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/eqsubst.ML Sat Jul 27 16:35:51 2013 +0200
@@ -252,7 +252,7 @@
RW_Inst.rw ctxt m rule conclthm
|> unfix_frees cfvs
|> Conv.fconv_rule Drule.beta_eta_conversion
- |> (fn r => Tactic.rtac r i st);
+ |> (fn r => rtac 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 *)
@@ -334,8 +334,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))
- (Tactic.dtac preelimrule i st2)
+ Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
end;
--- a/src/Tools/induct.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/induct.ML Sat Jul 27 16:35:51 2013 +0200
@@ -534,10 +534,10 @@
val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
-val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
+val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
val inner_atomize_tac =
- Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
+ rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
(* rulify *)
@@ -554,10 +554,10 @@
in (thy, Logic.list_implies (map rulify As, rulify B)) end;
val rulify_tac =
- Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
- Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN'
+ rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
+ rewrite_goal_tac Induct_Args.rulify_fallback THEN'
Goal.conjunction_tac THEN_ALL_NEW
- (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
+ (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
(* prepare rule *)
--- a/src/Tools/intuitionistic.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/intuitionistic.ML Sat Jul 27 16:35:51 2013 +0200
@@ -20,7 +20,7 @@
val remdups_tac = SUBGOAL (fn (g, i) =>
let val prems = Logic.strip_assums_hyp g in
REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
- (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
+ (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
end);
fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;