--- a/src/CCL/Wfd.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/CCL/Wfd.thy Thu Apr 12 18:39:19 2012 +0200
@@ -493,26 +493,19 @@
subsection {* Evaluation *}
ML {*
-
-local
- structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules");
-in
+structure Eval_Rules =
+ Named_Thms(val name = @{binding eval} val description = "evaluation rules");
fun eval_tac ths =
Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
- DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
+ DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1));
+*}
+setup Eval_Rules.setup
-val eval_setup =
- Data.setup #>
- Method.setup @{binding eval}
- (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)))
- "evaluation";
-
-end;
-
+method_setup eval = {*
+ Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))
*}
-setup eval_setup
lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Apr 12 18:39:19 2012 +0200
@@ -762,7 +762,7 @@
method_setup prepare = {*
Scan.succeed (K (SIMPLE_METHOD ShoupRubin.prepare_tac)) *}
- "to launch a few simple facts that'll help the simplifier"
+ "to launch a few simple facts that will help the simplifier"
method_setup parts_prepare = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Apr 12 18:39:19 2012 +0200
@@ -771,7 +771,7 @@
method_setup prepare = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
- "to launch a few simple facts that'll help the simplifier"
+ "to launch a few simple facts that will help the simplifier"
method_setup parts_prepare = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Thu Apr 12 18:39:19 2012 +0200
@@ -45,12 +45,12 @@
in tac ctxt (thms @ facts) end))
val setup_boogie = Method.setup @{binding boogie} (boogie_method false)
- ("Applies an SMT solver to the current goal " ^
- "using the current set of Boogie background axioms")
+ "apply an SMT solver to the current goal \
+ \using the current set of Boogie background axioms"
val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true)
- ("Applies an SMT solver to all goals " ^
- "using the current set of Boogie background axioms")
+ "apply an SMT solver to all goals \
+ \using the current set of Boogie background axioms"
local
@@ -96,7 +96,7 @@
in
val setup_boogie_cases = Method.setup @{binding boogie_cases}
(Scan.succeed boogie_cases)
- "Prepares a set of Boogie assertions for case-based proofs"
+ "prepare a set of Boogie assertions for case-based proofs"
end
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Apr 12 18:39:19 2012 +0200
@@ -314,6 +314,9 @@
use "commutative_ring_tac.ML"
-setup Commutative_Ring_Tac.setup
+
+method_setup comm_ring = {*
+ Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
+*} "reflective decision procedure for equalities over commutative rings"
end
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Apr 12 18:39:19 2012 +0200
@@ -2005,7 +2005,12 @@
*}
use "cooper_tac.ML"
-setup "Cooper_Tac.setup"
+
+method_setup cooper = {*
+ Args.mode "no_quantify" >>
+ (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
+*} "decision procedure for linear integer arithmetic"
+
text {* Tests *}
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Apr 12 18:39:19 2012 +0200
@@ -2004,7 +2004,12 @@
*}
use "ferrack_tac.ML"
-setup Ferrack_Tac.setup
+
+method_setup rferrack = {*
+ Args.mode "no_quantify" >>
+ (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
+*} "decision procedure for linear real arithmetic"
+
lemma
fixes x :: real
--- a/src/HOL/Decision_Procs/MIR.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Apr 12 18:39:19 2012 +0200
@@ -5635,7 +5635,12 @@
*}
use "mir_tac.ML"
-setup "Mir_Tac.setup"
+
+method_setup mir = {*
+ Args.mode "no_quantify" >>
+ (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
+*} "decision procedure for MIR arithmetic"
+
lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
by mir
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Apr 12 18:39:19 2012 +0200
@@ -7,7 +7,6 @@
signature COMMUTATIVE_RING_TAC =
sig
val tac: Proof.context -> int -> tactic
- val setup: theory -> theory
end
structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
@@ -98,8 +97,4 @@
THEN (simp_tac cring_ss i)
end);
-val setup =
- Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o tac))
- "reflective decision procedure for equalities over commutative rings";
-
end;
--- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 12 18:39:19 2012 +0200
@@ -6,7 +6,6 @@
sig
val trace: bool Unsynchronized.ref
val linz_tac: Proof.context -> bool -> int -> tactic
- val setup: theory -> theory
end
structure Cooper_Tac: COOPER_TAC =
@@ -115,15 +114,4 @@
| _ => (pre_thm, assm_tac i)
in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
-val setup =
- Method.setup @{binding cooper}
- let
- val parse_flag = Args.$$$ "no_quantify" >> K (K false)
- in
- Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
- curry (Library.foldl op |>) true) >>
- (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q))
- end
- "decision procedure for linear integer arithmetic";
-
end
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Thu Apr 12 18:39:19 2012 +0200
@@ -6,7 +6,6 @@
sig
val trace: bool Unsynchronized.ref
val linr_tac: Proof.context -> bool -> int -> tactic
- val setup: theory -> theory
end
structure Ferrack_Tac =
@@ -96,10 +95,4 @@
| _ => (pre_thm, assm_tac i)
in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
-val setup =
- Method.setup @{binding rferrack}
- (Args.mode "no_quantify" >> (fn q => fn ctxt =>
- SIMPLE_METHOD' (linr_tac ctxt (not q))))
- "decision procedure for linear real arithmetic";
-
end
--- a/src/HOL/Decision_Procs/mir_tac.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Thu Apr 12 18:39:19 2012 +0200
@@ -6,7 +6,6 @@
sig
val trace: bool Unsynchronized.ref
val mir_tac: Proof.context -> bool -> int -> tactic
- val setup: theory -> theory
end
structure Mir_Tac =
@@ -143,15 +142,4 @@
| _ => (pre_thm, assm_tac i)
in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
-val setup =
- Method.setup @{binding mir}
- let
- val parse_flag = Args.$$$ "no_quantify" >> K (K false)
- in
- Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
- curry (Library.foldl op |>) true) >>
- (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q))
- end
- "decision procedure for MIR arithmetic";
-
end
--- a/src/HOL/FunDef.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/FunDef.thy Thu Apr 12 18:39:19 2012 +0200
@@ -110,14 +110,21 @@
use "Tools/Function/relation.ML"
use "Tools/Function/function.ML"
use "Tools/Function/pat_completeness.ML"
+
+method_setup pat_completeness = {*
+ Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
+*} "prove completeness of datatype patterns"
+
use "Tools/Function/fun.ML"
use "Tools/Function/induction_schema.ML"
+method_setup induction_schema = {*
+ Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
+*} "prove an induction principle"
+
setup {*
Function.setup
- #> Pat_Completeness.setup
#> Function_Fun.setup
- #> Induction_Schema.setup
*}
subsection {* Measure Functions *}
@@ -137,6 +144,12 @@
by (rule is_measure_trivial)
use "Tools/Function/lexicographic_order.ML"
+
+method_setup lexicographic_order = {*
+ Method.sections clasimp_modifiers >>
+ (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
+*} "termination prover for lexicographic orderings"
+
setup Lexicographic_Order.setup
--- a/src/HOL/Groebner_Basis.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy Thu Apr 12 18:39:19 2012 +0200
@@ -43,8 +43,20 @@
use "Tools/groebner.ML"
-method_setup algebra = Groebner.algebra_method
- "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
+method_setup algebra = {*
+ let
+ fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+ val addN = "add"
+ val delN = "del"
+ val any_keyword = keyword addN || keyword delN
+ val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+ in
+ Scan.optional (keyword addN |-- thms) [] --
+ Scan.optional (keyword delN |-- thms) [] >>
+ (fn (add_ths, del_ths) => fn ctxt =>
+ SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
+ end
+*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
declare dvd_def[algebra]
declare dvd_eq_mod_eq_0[symmetric, algebra]
--- a/src/HOL/HOLCF/Fixrec.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy Thu Apr 12 18:39:19 2012 +0200
@@ -230,7 +230,9 @@
use "Tools/holcf_library.ML"
use "Tools/fixrec.ML"
-setup {* Fixrec.setup *}
+method_setup fixrec_simp = {*
+ Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
+*} "pattern prover for fixrec constants"
setup {*
Fixrec.add_matchers
--- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu Apr 12 18:39:19 2012 +0200
@@ -12,7 +12,6 @@
-> (bool * (Attrib.binding * string)) list -> local_theory -> local_theory
val add_matchers: (string * string) list -> theory -> theory
val fixrec_simp_tac: Proof.context -> int -> tactic
- val setup: theory -> theory
end
structure Fixrec : FIXREC =
@@ -406,9 +405,4 @@
(Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
>> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
-val setup =
- Method.setup @{binding fixrec_simp}
- (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
- "pattern prover for fixrec constants"
-
end
--- a/src/HOL/Library/Countable.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Library/Countable.thy Thu Apr 12 18:39:19 2012 +0200
@@ -269,8 +269,7 @@
by - (rule exI)
qed
-method_setup countable_datatype = {*
-let
+ML {*
fun countable_tac ctxt =
SUBGOAL (fn (goal, i) =>
let
@@ -297,9 +296,10 @@
etac induct_thm i,
REPEAT (resolve_tac rules i ORELSE atac i)]) 1
end)
-in
+*}
+
+method_setup countable_datatype = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt))
-end
*} "prove countable class instances for datatypes"
hide_const (open) finite_item nth_item
--- a/src/HOL/Library/Eval_Witness.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Apr 12 18:39:19 2012 +0200
@@ -77,8 +77,8 @@
method_setup eval_witness = {*
Scan.lift (Scan.repeat Args.name) >>
- (fn ws => K (SIMPLE_METHOD'
- (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
+ (fn ws => K (SIMPLE_METHOD'
+ (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
*} "evaluation with ML witnesses"
--- a/src/HOL/Limits.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Limits.thy Thu Apr 12 18:39:19 2012 +0200
@@ -112,7 +112,8 @@
qed
ML {*
- fun ev_elim_tac ctxt thms thm = let
+ fun eventually_elim_tac ctxt thms thm =
+ let
val thy = Proof_Context.theory_of ctxt
val mp_thms = thms RL [@{thm eventually_rev_mp}]
val raw_elim_thm =
@@ -124,13 +125,11 @@
in
CASES cases (rtac raw_elim_thm 1) thm
end
-
- fun eventually_elim_setup name =
- Method.setup name (Scan.succeed (fn ctxt => METHOD_CASES (ev_elim_tac ctxt)))
- "elimination of eventually quantifiers"
*}
-setup {* eventually_elim_setup @{binding "eventually_elim"} *}
+method_setup eventually_elim = {*
+ Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
+*} "elimination of eventually quantifiers"
subsection {* Finer-than relation *}
--- a/src/HOL/NSA/StarDef.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy Thu Apr 12 18:39:19 2012 +0200
@@ -91,6 +91,12 @@
use "transfer.ML"
setup Transfer_Principle.setup
+method_setup transfer = {*
+ Attrib.thms >> (fn ths => fn ctxt =>
+ SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))
+*} "transfer principle"
+
+
text {* Transfer introduction rules. *}
lemma transfer_ex [transfer_intro]:
--- a/src/HOL/NSA/transfer.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/NSA/transfer.ML Thu Apr 12 18:39:19 2012 +0200
@@ -112,8 +112,6 @@
Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
"declaration of transfer unfolding rule" #>
Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
- "declaration of transfer refolding rule" #>
- Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt =>
- SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle";
+ "declaration of transfer refolding rule"
end;
--- a/src/HOL/Orderings.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Orderings.thy Thu Apr 12 18:39:19 2012 +0200
@@ -312,7 +312,7 @@
signature ORDERS =
sig
val print_structures: Proof.context -> unit
- val setup: theory -> theory
+ val attrib_setup: theory -> theory
val order_tac: Proof.context -> thm list -> int -> tactic
end;
@@ -414,19 +414,15 @@
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_structures o Toplevel.context_of)));
-
-(** Setup **)
-
-val setup =
- Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
- "transitivity reasoner" #>
- attrib_setup;
-
end;
*}
-setup Orders.setup
+setup Orders.attrib_setup
+
+method_setup order = {*
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
+*} "transitivity reasoner"
text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
--- a/src/HOL/Presburger.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Presburger.thy Thu Apr 12 18:39:19 2012 +0200
@@ -387,10 +387,25 @@
by (simp cong: conj_cong)
use "Tools/Qelim/cooper.ML"
-
setup Cooper.setup
-method_setup presburger = "Cooper.method" "Cooper's algorithm for Presburger arithmetic"
+method_setup presburger = {*
+ let
+ fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+ fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
+ val addN = "add"
+ val delN = "del"
+ val elimN = "elim"
+ val any_keyword = keyword addN || keyword delN || simple_keyword elimN
+ val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+ in
+ Scan.optional (simple_keyword elimN >> K false) true --
+ Scan.optional (keyword addN |-- thms) [] --
+ Scan.optional (keyword delN |-- thms) [] >>
+ (fn ((elim, add_ths), del_ths) => fn ctxt =>
+ SIMPLE_METHOD' (Cooper.tac elim add_ths del_ths ctxt))
+ end
+*} "Cooper's algorithm for Presburger arithmetic"
declare dvd_eq_mod_eq_0[symmetric, presburger]
declare mod_1[presburger]
--- a/src/HOL/Tools/Function/induction_schema.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Thu Apr 12 18:39:19 2012 +0200
@@ -9,7 +9,6 @@
val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
-> Proof.context -> thm list -> tactic
val induction_schema_tac : Proof.context -> thm list -> tactic
- val setup : theory -> theory
end
@@ -395,8 +394,4 @@
fun induction_schema_tac ctxt =
mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
-val setup =
- Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
- "proves an induction principle"
-
end
--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Apr 12 18:39:19 2012 +0200
@@ -9,8 +9,6 @@
sig
val lex_order_tac : bool -> Proof.context -> tactic -> tactic
val lexicographic_order_tac : bool -> Proof.context -> tactic
- val lexicographic_order : Proof.context -> Proof.method
-
val setup: theory -> theory
end
@@ -218,12 +216,7 @@
lex_order_tac quiet ctxt
(auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
-val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
-
val setup =
- Method.setup @{binding lexicographic_order}
- (Method.sections clasimp_modifiers >> (K lexicographic_order))
- "termination prover for lexicographic orderings"
- #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
+ Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
end;
--- a/src/HOL/Tools/Function/pat_completeness.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML Thu Apr 12 18:39:19 2012 +0200
@@ -7,11 +7,8 @@
signature PAT_COMPLETENESS =
sig
val pat_completeness_tac: Proof.context -> int -> tactic
- val pat_completeness: Proof.context -> Proof.method
val prove_completeness : theory -> term list -> term -> term list list ->
term list list -> thm
-
- val setup : theory -> theory
end
structure Pat_Completeness : PAT_COMPLETENESS =
@@ -153,11 +150,4 @@
end
handle COMPLETENESS => no_tac)
-
-val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac
-
-val setup =
- Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
- "Completeness prover for datatype patterns"
-
end
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Apr 12 18:39:19 2012 +0200
@@ -13,7 +13,6 @@
exception COOPER of string
val conv: Proof.context -> conv
val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
- val method: (Proof.context -> Method.method) context_parser
val setup: theory -> theory
end;
@@ -857,23 +856,6 @@
THEN_ALL_NEW finish_tac elim
end;
-val method =
- let
- fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
- fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
- val addN = "add"
- val delN = "del"
- val elimN = "elim"
- val any_keyword = keyword addN || keyword delN || simple_keyword elimN
- val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
- in
- Scan.optional (simple_keyword elimN >> K false) true --
- Scan.optional (keyword addN |-- thms) [] --
- Scan.optional (keyword delN |-- thms) [] >>
- (fn ((elim, add_ths), del_ths) => fn ctxt =>
- SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
- end;
-
(* theory setup *)
--- a/src/HOL/Tools/groebner.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/groebner.ML Thu Apr 12 18:39:19 2012 +0200
@@ -16,7 +16,6 @@
val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
- val algebra_method: (Proof.context -> Method.method) context_parser
end
structure Groebner : GROEBNER =
@@ -1027,21 +1026,4 @@
fun algebra_tac add_ths del_ths ctxt i =
ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
-local
-
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
-val addN = "add"
-val delN = "del"
-val any_keyword = keyword addN || keyword delN
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-
-in
-
-val algebra_method = ((Scan.optional (keyword addN |-- thms) []) --
- (Scan.optional (keyword delN |-- thms) [])) >>
- (fn (add_ths, del_ths) => fn ctxt =>
- SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
-
end;
-
-end;
--- a/src/HOL/ex/SAT_Examples.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Thu Apr 12 18:39:19 2012 +0200
@@ -80,11 +80,9 @@
ML {* sat.trace_sat := false; *}
ML {* quick_and_dirty := false; *}
-method_setup rawsat =
- {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
- "SAT solver (no preprocessing)"
-
-(* ML {* Toplevel.profiling := 1; *} *)
+method_setup rawsat = {*
+ Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
+*} "SAT solver (no preprocessing)"
(* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
@@ -512,8 +510,6 @@
(as of 2006-08-30, on a 2.5 GHz Pentium 4)
*)
-(* ML {* Toplevel.profiling := 0; *} *)
-
text {*
Function {\tt benchmark} takes the name of an existing DIMACS CNF
file, parses this file, passes the problem to a SAT solver, and checks