# HG changeset patch # User wenzelm # Date 1236984967 -3600 # Node ID 3ec2d35b380fdd074969c66327ecd03adcf3efcc # Parent c4728771f04f26537449ad24bcdea4ab4f21a3ac# Parent bca05b17b6186a6829ac8fe9c22f8f50872089e9 merged diff -r c4728771f04f -r 3ec2d35b380f doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/doc-src/IsarRef/Thy/Proof.thy Fri Mar 13 23:56:07 2009 +0100 @@ -895,11 +895,10 @@ %FIXME proper antiquotations {\footnotesize \begin{verbatim} - Method.no_args (Method.METHOD (fn facts => foobar_tac)) - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) - Method.thms_ctxt_args (fn thms => fn ctxt => - Method.METHOD (fn facts => foobar_tac)) + Method.no_args (METHOD (fn facts => foobar_tac)) + Method.thms_args (fn thms => METHOD (fn facts => foobar_tac)) + Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac)) + Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac)) \end{verbatim} } diff -r c4728771f04f -r 3ec2d35b380f doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Mar 13 19:18:07 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Mar 13 23:56:07 2009 +0100 @@ -899,11 +899,10 @@ %FIXME proper antiquotations {\footnotesize \begin{verbatim} - Method.no_args (Method.METHOD (fn facts => foobar_tac)) - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) - Method.thms_ctxt_args (fn thms => fn ctxt => - Method.METHOD (fn facts => foobar_tac)) + Method.no_args (METHOD (fn facts => foobar_tac)) + Method.thms_args (fn thms => METHOD (fn facts => foobar_tac)) + Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac)) + Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac)) \end{verbatim} } diff -r c4728771f04f -r 3ec2d35b380f doc-src/TutorialI/Protocol/Event.thy --- a/doc-src/TutorialI/Protocol/Event.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Event.thy Fri Mar 13 23:56:07 2009 +0100 @@ -287,7 +287,7 @@ intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) method_setup analz_mono_contra = {* - Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} + Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} @@ -344,7 +344,7 @@ *} method_setup synth_analz_mono_contra = {* - Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} + Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} "for proving theorems of the form X \ synth (analz (knows Spy evs)) --> P" (*>*) diff -r c4728771f04f -r 3ec2d35b380f doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Message.thy Fri Mar 13 23:56:07 2009 +0100 @@ -919,18 +919,15 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} + Method.ctxt_args (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} + Method.ctxt_args (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} + Method.ctxt_args (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *} "for debugging spy_analz" diff -r c4728771f04f -r 3ec2d35b380f doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 23:56:07 2009 +0100 @@ -161,8 +161,7 @@ resolve_tac [refl, conjI, @{thm Nonce_supply}])); *} -method_setup possibility = {* - Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} +method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *} "for proving possibility theorems" end diff -r c4728771f04f -r 3ec2d35b380f src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/CCL/Wfd.thy Fri Mar 13 23:56:07 2009 +0100 @@ -504,8 +504,9 @@ val eval_setup = Data.setup #> - Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt => - Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")]; + Method.setup @{binding eval} + (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (CHANGED (eval_tac ctxt ths)))) + "evaluation"; end; diff -r c4728771f04f -r 3ec2d35b380f src/Cube/Example.thy --- a/src/Cube/Example.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Cube/Example.thy Fri Mar 13 23:56:07 2009 +0100 @@ -15,18 +15,18 @@ *} method_setup depth_solve = {* - Method.thms_args (fn thms => Method.METHOD (fn facts => + Method.thms_args (fn thms => METHOD (fn facts => (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))) *} "" method_setup depth_solve1 = {* - Method.thms_args (fn thms => Method.METHOD (fn facts => + Method.thms_args (fn thms => METHOD (fn facts => (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))) *} "" method_setup strip_asms = {* let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in - Method.thms_args (fn thms => Method.METHOD (fn facts => + Method.thms_args (fn thms => METHOD (fn facts => REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))) end *} "" diff -r c4728771f04f -r 3ec2d35b380f src/FOL/ex/Iff_Oracle.thy --- a/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 23:56:07 2009 +0100 @@ -53,7 +53,7 @@ method_setup iff = {* Method.simple_args OuterParse.nat (fn n => fn ctxt => - Method.SIMPLE_METHOD + SIMPLE_METHOD (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) handle Fail _ => no_tac)) *} "iff oracle" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 13 23:56:07 2009 +0100 @@ -222,7 +222,7 @@ *} (* Note: r_one is not necessary in ring_ss *) method_setup ring = - {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *} + {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *} {* computes distributive normal form in rings *} diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Algebra/ringsimp.ML Fri Mar 13 23:56:07 2009 +0100 @@ -72,8 +72,8 @@ (** Setup **) val setup = - Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac), - "normalisation of algebraic structure")] #> + Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac)) + "normalisation of algebraic structure" #> Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")]; end; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/Event.thy Fri Mar 13 23:56:07 2009 +0100 @@ -289,7 +289,7 @@ *} method_setup analz_mono_contra = {* - Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} + Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} @@ -310,7 +310,7 @@ *} method_setup synth_analz_mono_contra = {* - Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} + Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} "for proving theorems of the form X \ synth (analz (knows Spy evs)) --> P" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/Message.thy Fri Mar 13 23:56:07 2009 +0100 @@ -941,18 +941,15 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Message.gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} + Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Message.atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} + Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Message.Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} + Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *} "for debugging spy_analz" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/OtwayReesBella.thy --- a/src/HOL/Auth/OtwayReesBella.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/OtwayReesBella.thy Fri Mar 13 23:56:07 2009 +0100 @@ -137,7 +137,7 @@ *} method_setup parts_explicit = {* - Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *} + Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *} "to explicitly state that some message components belong to parts knows Spy" @@ -258,7 +258,7 @@ method_setup analz_freshCryptK = {* Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD + (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}), ALLGOALS (asm_simp_tac @@ -268,7 +268,7 @@ method_setup disentangle = {* Method.no_args - (Method.SIMPLE_METHOD + (SIMPLE_METHOD (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac))) *} "for eliminating conjunctions, disjunctions and the like" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/Public.thy Fri Mar 13 23:56:07 2009 +0100 @@ -425,7 +425,7 @@ method_setup analz_freshK = {* Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD + (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *} @@ -435,13 +435,11 @@ subsection{*Specialized Methods for Possibility Theorems*} method_setup possibility = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Public.possibility_tac ctxt)) *} + Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *} "for proving possibility theorems" method_setup basic_possibility = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Public.basic_possibility_tac ctxt)) *} + Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *} "for proving possibility theorems" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/Shared.thy Fri Mar 13 23:56:07 2009 +0100 @@ -239,20 +239,18 @@ method_setup analz_freshK = {* Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD + (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *} "for proving the Session Key Compromise theorem" method_setup possibility = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Shared.possibility_tac ctxt)) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *} "for proving possibility theorems" method_setup basic_possibility = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *} "for proving possibility theorems" lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Mar 13 23:56:07 2009 +0100 @@ -769,15 +769,15 @@ *} method_setup prepare = {* - Method.no_args (Method.SIMPLE_METHOD ShoupRubin.prepare_tac) *} + Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *} "to launch a few simple facts that'll help the simplifier" method_setup parts_prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *} "additional facts to reason about parts" method_setup analz_prepare = {* - Method.no_args (Method.SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *} + Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *} "additional facts to reason about analz" @@ -823,7 +823,7 @@ method_setup sc_analz_freshK = {* Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD + (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Mar 13 23:56:07 2009 +0100 @@ -777,15 +777,15 @@ *} method_setup prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *} "to launch a few simple facts that'll help the simplifier" method_setup parts_prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *} "additional facts to reason about parts" method_setup analz_prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *} "additional facts to reason about analz" @@ -832,7 +832,7 @@ method_setup sc_analz_freshK = {* Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD + (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Fri Mar 13 23:56:07 2009 +0100 @@ -408,7 +408,7 @@ method_setup analz_freshK = {* Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD + (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *} @@ -416,12 +416,12 @@ method_setup possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *} + SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *} "for proving possibility theorems" method_setup basic_possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *} + SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *} "for proving possibility theorems" lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Code_Setup.thy --- a/src/HOL/Code_Setup.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Code_Setup.thy Fri Mar 13 23:56:07 2009 +0100 @@ -226,7 +226,7 @@ *} ML {* -fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' +fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt) THEN' rtac TrueI)) *} @@ -237,7 +237,7 @@ method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *} "solve goal by evaluation" -method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD') +method_setup normalization = {* (Method.no_args o SIMPLE_METHOD') (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k))) *} "solve goal by normalization" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Fri Mar 13 23:56:07 2009 +0100 @@ -2499,7 +2499,7 @@ method_setup approximation = {* fn src => Method.syntax Args.term src #> (fn (prec, ctxt) => let - in Method.SIMPLE_METHOD' (fn i => + in SIMPLE_METHOD' (fn i => (DETERM (reify_uneq ctxt i) THEN rule_uneq ctxt prec i THEN Simplifier.asm_full_simp_tac bounded_by_simpset i diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Mar 13 23:56:07 2009 +0100 @@ -295,7 +295,7 @@ use "~~/src/HOL/Tools/Qelim/langford.ML" method_setup dlo = {* - Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac) + Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac) *} "Langford's algorithm for quantifier elimination in dense linear orders" @@ -546,7 +546,7 @@ use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML" method_setup ferrack = {* - Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac) + Method.ctxt_args (SIMPLE_METHOD' o FerranteRackoff.dlo_tac) *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" subsection {* Ferrante and Rackoff algorithm over ordered fields *} diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 13 23:56:07 2009 +0100 @@ -121,11 +121,10 @@ Method.simple_args (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> curry (Library.foldl op |>) true) - (fn q => fn ctxt => meth ctxt q 1) + (fn q => fn ctxt => meth ctxt q) end; -fun linz_method ctxt q i = Method.METHOD (fn facts => - Method.insert_tac facts 1 THEN linz_tac ctxt q i); +fun linz_method ctxt q = SIMPLE_METHOD' (linz_tac ctxt q); val setup = Method.add_method ("cooper", diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 13 23:56:07 2009 +0100 @@ -100,7 +100,7 @@ fun linr_meth src = Method.syntax (Args.mode "no_quantify") src - #> (fn (q, ctxt) => Method.SIMPLE_METHOD' (linr_tac ctxt (not q))); + #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q))); val setup = Method.add_method ("rferrack", linr_meth, diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 13 23:56:07 2009 +0100 @@ -150,11 +150,10 @@ Method.simple_args (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> curry (Library.foldl op |>) true) - (fn q => fn ctxt => meth ctxt q 1) + (fn q => fn ctxt => meth ctxt q) end; -fun mir_method ctxt q i = Method.METHOD (fn facts => - Method.insert_tac facts 1 THEN mir_tac ctxt q i); +fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q); val setup = Method.add_method ("mir", diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Fri Mar 13 23:56:07 2009 +0100 @@ -253,7 +253,7 @@ method_setup sring_norm = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt)) + Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac) *} "semiring normalizer" @@ -431,7 +431,7 @@ ((Scan.optional (keyword addN |-- thms) []) -- (Scan.optional (keyword delN |-- thms) [])) src #> (fn ((add_ths, del_ths), ctxt) => - Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths 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] diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Hoare/Hoare.thy --- a/src/HOL/Hoare/Hoare.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Hoare/Hoare.thy Fri Mar 13 23:56:07 2009 +0100 @@ -234,12 +234,12 @@ use "hoare_tac.ML" method_setup vcg = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} "verification condition generator" method_setup vcg_simp = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *} + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *} "verification condition generator plus simplification" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Hoare/HoareAbort.thy --- a/src/HOL/Hoare/HoareAbort.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Hoare/HoareAbort.thy Fri Mar 13 23:56:07 2009 +0100 @@ -246,12 +246,12 @@ use "hoare_tac.ML" method_setup vcg = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} + Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} "verification condition generator" method_setup vcg_simp = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *} + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *} "verification condition generator plus simplification" (* Special syntax for guarded statements and guarded array updates: *) diff -r c4728771f04f -r 3ec2d35b380f src/HOL/HoareParallel/OG_Tactics.thy --- a/src/HOL/HoareParallel/OG_Tactics.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/HoareParallel/OG_Tactics.thy Fri Mar 13 23:56:07 2009 +0100 @@ -465,21 +465,21 @@ Isabelle proofs. *} method_setup oghoare = {* - Method.no_args (Method.SIMPLE_METHOD' oghoare_tac) *} + Method.no_args (SIMPLE_METHOD' oghoare_tac) *} "verification condition generator for the oghoare logic" method_setup annhoare = {* - Method.no_args (Method.SIMPLE_METHOD' annhoare_tac) *} + Method.no_args (SIMPLE_METHOD' annhoare_tac) *} "verification condition generator for the ann_hoare logic" method_setup interfree_aux = {* - Method.no_args (Method.SIMPLE_METHOD' interfree_aux_tac) *} + Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *} "verification condition generator for interference freedom tests" text {* Tactics useful for dealing with the generated verification conditions: *} method_setup conjI_tac = {* - Method.no_args (Method.SIMPLE_METHOD' (conjI_Tac (K all_tac))) *} + Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *} "verification condition generator for interference freedom tests" ML {* @@ -490,7 +490,7 @@ *} method_setup disjE_tac = {* - Method.no_args (Method.SIMPLE_METHOD' (disjE_Tac (K all_tac))) *} + Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *} "verification condition generator for interference freedom tests" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Import/import_package.ML --- a/src/HOL/Import/import_package.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Import/import_package.ML Fri Mar 13 23:56:07 2009 +0100 @@ -73,7 +73,7 @@ let val thy = ProofContext.theory_of ctxt in - Method.SIMPLE_METHOD (import_tac arg thy) + SIMPLE_METHOD (import_tac arg thy) end) val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Import/shuffler.ML Fri Mar 13 23:56:07 2009 +0100 @@ -656,7 +656,7 @@ let val thy = ProofContext.theory_of ctxt in - Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms)) + SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms)) end fun search_meth ctxt = @@ -664,7 +664,7 @@ val thy = ProofContext.theory_of ctxt val prems = Assumption.all_prems_of ctxt in - Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems)) + SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems)) end fun add_shuffle_rule thm thy = diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Isar_examples/Hoare.thy --- a/src/HOL/Isar_examples/Hoare.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Isar_examples/Hoare.thy Fri Mar 13 23:56:07 2009 +0100 @@ -455,7 +455,7 @@ method_setup hoare = {* Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD' + (SIMPLE_METHOD' (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *} "verification condition generator for Hoare logic" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Fri Mar 13 23:56:07 2009 +0100 @@ -134,7 +134,7 @@ (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) THEN' asm_full_simp_tac (ss2 addsimps ths) in - Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac) + Method.thms_args (SIMPLE_METHOD' o vector_arith_tac) end *} "Lifts trivial vector statements to real arith statements" @@ -948,7 +948,7 @@ use "normarith.ML" -method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac) +method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac) *} "Proves simple linear statements about vector norms" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Library/Eval_Witness.thy --- a/src/HOL/Library/Eval_Witness.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Library/Eval_Witness.thy Fri Mar 13 23:56:07 2009 +0100 @@ -84,7 +84,7 @@ in Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ => - Method.SIMPLE_METHOD' (eval_tac ws)) + SIMPLE_METHOD' (eval_tac ws)) end *} "Evaluation with ML witnesses" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Library/Reflection.thy --- a/src/HOL/Library/Reflection.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Library/Reflection.thy Fri Mar 13 23:56:07 2009 +0100 @@ -19,7 +19,7 @@ method_setup reify = {* fn src => Method.syntax (Attrib.thms -- Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #> - (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to)) + (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to)) *} "partial automatic reification" method_setup reflection = {* @@ -38,7 +38,7 @@ val (ceqs,cths) = Reify_Data.get ctxt val corr_thms = ths@cths val raw_eqs = eqs@ceqs - in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) + in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end) end *} "reflection method" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Fri Mar 13 23:56:07 2009 +0100 @@ -978,7 +978,7 @@ val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym] val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}] fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2 - in Method.thms_args (Method.SIMPLE_METHOD' o tac) end + in Method.thms_args (SIMPLE_METHOD' o tac) end *} "Reduces goals about net" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Library/comm_ring.ML --- a/src/HOL/Library/comm_ring.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Library/comm_ring.ML Fri Mar 13 23:56:07 2009 +0100 @@ -101,7 +101,7 @@ end); val comm_ring_meth = - Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac); + Method.ctxt_args (SIMPLE_METHOD' o comm_ring_tac); val setup = Method.add_method ("comm_ring", comm_ring_meth, diff -r c4728771f04f -r 3ec2d35b380f src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/NSA/transfer.ML Fri Mar 13 23:56:07 2009 +0100 @@ -116,6 +116,6 @@ ("transfer_refold", Attrib.add_del_args refold_add refold_del, "declaration of transfer refolding rule")] #> Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt => - Method.SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle"); + SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle"); end; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 13 23:56:07 2009 +0100 @@ -204,4 +204,4 @@ val setup_fresh_fun_simp = Method.simple_args options_syntax - (fn b => fn _ => Method.SIMPLE_METHOD (fresh_fun_tac b 1)) + (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1)) diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Nominal/nominal_induct.ML Fri Mar 13 23:56:07 2009 +0100 @@ -8,7 +8,7 @@ val nominal_induct_tac: Proof.context -> (binding option * term) option list list -> (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> RuleCases.cases_tactic - val nominal_induct_method: Method.src -> Proof.context -> Method.method + val nominal_induct_method: Method.src -> Proof.context -> Proof.method end = struct @@ -157,7 +157,7 @@ (P.and_list' (Scan.repeat (unless_more_args def_inst)) -- avoiding -- fixing -- rule_spec) src #> (fn ((((x, y), z), w), ctxt) => - Method.RAW_METHOD_CASES (fn facts => + RAW_METHOD_CASES (fn facts => HEADGOAL (nominal_induct_tac ctxt x y z w facts))); end; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Fri Mar 13 23:56:07 2009 +0100 @@ -400,7 +400,7 @@ Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) || Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac)); -fun perm_simp_method (prems, tac) ctxt = Method.METHOD (fn facts => +fun perm_simp_method (prems, tac) ctxt = METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' ((CHANGED_PROP) oo tac) (local_simpset_of ctxt))); @@ -411,7 +411,7 @@ (* setup so that the simpset is used which is active at the moment when the tactic is called *) fun local_simp_meth_setup tac = Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers) - (Method.SIMPLE_METHOD' o tac o local_simpset_of) ; + (SIMPLE_METHOD' o tac o local_simpset_of) ; (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *) @@ -419,7 +419,7 @@ Method.sectioned_args (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l))) (Simplifier.simp_modifiers' @ Splitter.split_modifiers) - (fn _ => Method.SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of); + (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of); val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac; val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 13 23:56:07 2009 +0100 @@ -378,7 +378,7 @@ |> snd end) [goals] |> - Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ => + Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ => rewrite_goals_tac defs_thms THEN compose_tac (false, rule, length rule_prems) 1), Position.none)) |> Seq.hd diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Orderings.thy Fri Mar 13 23:56:07 2009 +0100 @@ -397,8 +397,7 @@ (** Setup **) val setup = - Method.add_methods - [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #> + Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #> Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]; end; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Presburger.thy Fri Mar 13 23:56:07 2009 +0100 @@ -460,7 +460,7 @@ (Scan.optional (keyword addN |-- thms) []) -- (Scan.optional (keyword delN |-- thms) [])) src #> (fn (((elim, add_ths), del_ths),ctxt) => - Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt)) + SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt)) end *} "Cooper's algorithm for Presburger arithmetic" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Prolog/HOHH.thy --- a/src/HOL/Prolog/HOHH.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Prolog/HOHH.thy Fri Mar 13 23:56:07 2009 +0100 @@ -11,11 +11,11 @@ begin method_setup ptac = - {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *} + {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *} "Basic Lambda Prolog interpreter" method_setup prolog = - {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *} + {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *} "Lambda Prolog interpreter" consts diff -r c4728771f04f -r 3ec2d35b380f src/HOL/SAT.thy --- a/src/HOL/SAT.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/SAT.thy Fri Mar 13 23:56:07 2009 +0100 @@ -28,10 +28,10 @@ ML {* structure sat = SATFunc(structure cnf = cnf); *} -method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *} +method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *} "SAT solver" -method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *} +method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *} "SAT solver (with definitional CNF)" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/SET-Protocol/EventSET.thy --- a/src/HOL/SET-Protocol/EventSET.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/SET-Protocol/EventSET.thy Fri Mar 13 23:56:07 2009 +0100 @@ -189,7 +189,7 @@ *} method_setup analz_mono_contra = {* - Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} + Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/SET-Protocol/MessageSET.thy Fri Mar 13 23:56:07 2009 +0100 @@ -941,17 +941,17 @@ method_setup spy_analz = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *} + SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *} "for debugging spy_analz" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/SET-Protocol/PublicSET.thy --- a/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 13 23:56:07 2009 +0100 @@ -372,7 +372,7 @@ method_setup possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *} + SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *} "for proving possibility theorems" diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Fri Mar 13 23:56:07 2009 +0100 @@ -149,7 +149,7 @@ thy |> Expression.sublocale_cmd name expr |> Proof.global_terminal_proof - (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE) + (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE) |> ProofContext.theory_of fun add_locale name expr elems thy = diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/function_package/auto_term.ML --- a/src/HOL/Tools/function_package/auto_term.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/function_package/auto_term.ML Fri Mar 13 23:56:07 2009 +0100 @@ -29,8 +29,9 @@ TRY (FundefCommon.apply_termination_rule ctxt i) THEN PRIMITIVE (inst_thm ctxt rel) -val setup = Method.add_methods - [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term), - "proves termination using a user-specified wellfounded relation")] +val setup = + Method.setup @{binding relation} + (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel))) + "proves termination using a user-specified wellfounded relation" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 13 23:56:07 2009 +0100 @@ -155,7 +155,7 @@ structure TerminationProver = GenericDataFun ( - type T = (Proof.context -> Method.method) + type T = Proof.context -> Proof.method val empty = (fn _ => error "Termination prover not configured") val extend = I fun merge _ (a,b) = b (* FIXME *) diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 23:56:07 2009 +0100 @@ -203,7 +203,7 @@ handle COMPLETENESS => no_tac) -fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt) +fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt) val by_pat_completeness_auto = Proof.global_future_terminal_proof @@ -300,8 +300,8 @@ end val setup = - Method.add_methods [("pat_completeness", Method.ctxt_args pat_completeness, - "Completeness prover for datatype patterns")] + Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness) + "Completeness prover for datatype patterns" #> Context.theory_map (FundefCommon.set_preproc sequential_preproc) diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/function_package/induction_scheme.ML --- a/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 23:56:07 2009 +0100 @@ -398,8 +398,8 @@ fun induct_scheme_tac ctxt = mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; -val setup = Method.add_methods - [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o induct_scheme_tac), - "proves an induction principle")] +val setup = + Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac)) + "proves an induction principle" end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 23:56:07 2009 +0100 @@ -218,7 +218,7 @@ TRY (FundefCommon.apply_termination_rule ctxt 1) THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)) -val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac +val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order, "termination prover for lexicographic orderings")] diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/function_package/scnp_reconstruct.ML --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Fri Mar 13 23:56:07 2009 +0100 @@ -10,7 +10,7 @@ val sizechange_tac : Proof.context -> tactic -> tactic - val decomp_scnp : ScnpSolve.label list -> Proof.context -> method + val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method val setup : theory -> theory @@ -408,7 +408,7 @@ val extra_simps = FundefCommon.TerminationSimps.get ctxt val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps) in - Method.SIMPLE_METHOD + SIMPLE_METHOD (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)) end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/inductive_package.ML Fri Mar 13 23:56:07 2009 +0100 @@ -460,9 +460,10 @@ val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop; -fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source -- - Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) [])) src - #> (fn ((raw_props, fixes), ctxt) => +val ind_cases = + Scan.lift (Scan.repeat1 Args.name_source -- + Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >> + (fn (raw_props, fixes) => fn ctxt => let val (_, ctxt') = Variable.add_fixes fixes ctxt; val props = Syntax.read_props ctxt' raw_props; @@ -933,8 +934,7 @@ (* setup theory *) val setup = - Method.add_methods [("ind_cases", ind_cases, - "dynamic case analysis on predicates")] #> + Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #> Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del, "declaration of monotonicity rule")]; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Fri Mar 13 23:56:07 2009 +0100 @@ -912,9 +912,8 @@ ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false, more_arith_tacs ctxt]; -fun arith_method src = - Method.syntax Args.bang_facts src - #> (fn (prems, ctxt) => Method.METHOD (fn facts => +val arith_method = Args.bang_facts >> + (fn prems => fn ctxt => METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts) THEN' arith_tac ctxt))); @@ -930,8 +929,7 @@ (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #> Context.mapping (setup_options #> - Method.add_methods - [("arith", arith_method, "decide linear arithmetic")] #> + Method.setup @{binding arith} arith_method "decide linear arithmetic" #> Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add, "declaration of split rules for arithmetic procedure")]) I; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/metis_tools.ML Fri Mar 13 23:56:07 2009 +0100 @@ -637,17 +637,16 @@ val metisF_tac = metis_general_tac ResAtp.Fol; val metisH_tac = metis_general_tac ResAtp.Hol; - fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt => - Method.SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths)); + fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment; val setup = type_lits_setup #> - Method.add_methods - [("metis", method ResAtp.Auto, "METIS for FOL & HOL problems"), - ("metisF", method ResAtp.Fol, "METIS for FOL problems"), - ("metisH", method ResAtp.Hol, "METIS for HOL problems"), - ("finish_clausify", - Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))), - "cleanup after conversion to clauses")]; + method @{binding metis} ResAtp.Auto "METIS for FOL & HOL problems" #> + method @{binding metisF} ResAtp.Fol "METIS for FOL problems" #> + method @{binding metisH} ResAtp.Hol "METIS for HOL problems" #> + Method.setup @{binding finish_clausify} + (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl)))) + "cleanup after conversion to clauses"; end; diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Tools/res_axioms.ML Fri Mar 13 23:56:07 2009 +0100 @@ -487,10 +487,10 @@ val thy = Thm.theory_of_thm st0 in (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end; -val meson_method_setup = Method.add_methods - [("meson", Method.thms_args (fn ths => - Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)), - "MESON resolution proof procedure")]; +val meson_method_setup = + Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn _ => + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths))) + "MESON resolution proof procedure"; (*** Converting a subgoal into negated conjecture clauses. ***) @@ -521,9 +521,9 @@ REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); -val setup_methods = Method.add_methods - [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), - "conversion of goal to conjecture clauses")]; +val setup_methods = + Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac))) + "conversion of goal to conjecture clauses"; (** Attribute for converting a theorem into clauses **) diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Transitive_Closure.thy Fri Mar 13 23:56:07 2009 +0100 @@ -695,16 +695,16 @@ (* Optional methods *) method_setup trancl = - {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *} + {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *} {* simple transitivity reasoner *} method_setup rtrancl = - {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *} + {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *} {* simple transitivity reasoner *} method_setup tranclp = - {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *} + {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *} {* simple transitivity reasoner (predicate version) *} method_setup rtranclp = - {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *} + {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *} {* simple transitivity reasoner (predicate version) *} end diff -r c4728771f04f -r 3ec2d35b380f src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Fri Mar 13 23:56:07 2009 +0100 @@ -321,7 +321,7 @@ *} method_setup record_auto = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt))) + Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt))) *} "" lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc" @@ -714,7 +714,7 @@ method_setup rename_client_map = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt))) + SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt))) *} "" text{*Lifting @{text Client_Increasing} to @{term systemState}*} diff -r c4728771f04f -r 3ec2d35b380f src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Mar 13 23:56:07 2009 +0100 @@ -125,7 +125,7 @@ method_setup ns_induct = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *} "for inductive reasoning about the Needham-Schroeder protocol" text{*Converts invariants into statements about reachable states*} diff -r c4728771f04f -r 3ec2d35b380f src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/UNITY/UNITY_Main.thy Fri Mar 13 23:56:07 2009 +0100 @@ -11,7 +11,7 @@ method_setup safety = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *} "for proving safety properties" method_setup ensures_tac = {* diff -r c4728771f04f -r 3ec2d35b380f src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Fri Mar 13 23:56:07 2009 +0100 @@ -530,7 +530,7 @@ *} method_setup uint_arith = - "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (uint_arith_tac ctxt 1))" + "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)" "solving word arithmetic via integers and arith" @@ -1086,7 +1086,7 @@ *} method_setup unat_arith = - "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (unat_arith_tac ctxt 1))" + "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)" "solving word arithmetic via natural numbers and arith" lemma no_plus_overflow_unat_size: diff -r c4728771f04f -r 3ec2d35b380f src/HOL/ex/Binary.thy --- a/src/HOL/ex/Binary.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/ex/Binary.thy Fri Mar 13 23:56:07 2009 +0100 @@ -174,7 +174,7 @@ simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *} method_setup binary_simp = {* - Method.no_args (Method.SIMPLE_METHOD' + Method.no_args (SIMPLE_METHOD' (full_simp_tac (HOL_basic_ss addsimps @{thms binary_simps} diff -r c4728771f04f -r 3ec2d35b380f src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/HOL/ex/SAT_Examples.thy Fri Mar 13 23:56:07 2009 +0100 @@ -83,7 +83,7 @@ ML {* reset quick_and_dirty; *} method_setup rawsat = - {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *} + {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *} "SAT solver (no preprocessing)" (* ML {* Toplevel.profiling := 1; *} *) diff -r c4728771f04f -r 3ec2d35b380f src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Provers/blast.ML Fri Mar 13 23:56:07 2009 +0100 @@ -56,7 +56,7 @@ uwrappers: (string * wrapper) list, safe0_netpair: netpair, safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair} - val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list + val cla_modifiers: Method.modifier parser list val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method end; diff -r c4728771f04f -r 3ec2d35b380f src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Provers/clasimp.ML Fri Mar 13 23:56:07 2009 +0100 @@ -62,8 +62,8 @@ val iff_add: attribute val iff_add': attribute val iff_del: attribute - val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list - val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list + val iff_modifiers: Method.modifier parser list + val clasimp_modifiers: Method.modifier parser list val clasimp_setup: theory -> theory end; @@ -290,10 +290,10 @@ (* methods *) -fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts => +fun clasimp_meth tac prems ctxt = METHOD (fn facts => ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt)); -fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts => +fun clasimp_meth' tac prems ctxt = METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt))); val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth; diff -r c4728771f04f -r 3ec2d35b380f src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Provers/classical.ML Fri Mar 13 23:56:07 2009 +0100 @@ -146,7 +146,7 @@ val haz_elim: int option -> attribute val haz_intro: int option -> attribute val rule_del: attribute - val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list + val cla_modifiers: Method.modifier parser list val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method @@ -971,11 +971,8 @@ (** proof methods **) -fun METHOD_CLASET tac ctxt = - Method.METHOD (tac ctxt (local_claset_of ctxt)); - -fun METHOD_CLASET' tac ctxt = - Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); +fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt)); +fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); local @@ -1021,10 +1018,10 @@ Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE), Args.del -- Args.colon >> K (I, rule_del)]; -fun cla_meth tac prems ctxt = Method.METHOD (fn facts => +fun cla_meth tac prems ctxt = METHOD (fn facts => ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); -fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => +fun cla_meth' tac prems ctxt = METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt))); val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; diff -r c4728771f04f -r 3ec2d35b380f src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Provers/hypsubst.ML Fri Mar 13 23:56:07 2009 +0100 @@ -284,9 +284,10 @@ (* theory setup *) val hypsubst_setup = - Method.add_methods - [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)), - "substitution using an assumption (improper)"), - ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")]; + Method.setup @{binding hypsubst} + (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)))) + "substitution using an assumption (improper)" #> + Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th)))) + "simple substitution"; end; diff -r c4728771f04f -r 3ec2d35b380f src/Provers/splitter.ML --- a/src/Provers/splitter.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Provers/splitter.ML Fri Mar 13 23:56:07 2009 +0100 @@ -39,7 +39,7 @@ val Delsplits : thm list -> unit val split_add: attribute val split_del: attribute - val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list + val split_modifiers : Method.modifier parser list val setup: theory -> theory end; @@ -472,16 +472,15 @@ Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add), Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; -fun split_meth src = - Method.syntax Attrib.thms src - #> (fn (ths, _) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)); +val split_meth = Attrib.thms >> + (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))); (* theory setup *) val setup = - (Attrib.add_attributes - [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #> - Method.add_methods [(splitN, split_meth, "apply case split rule")]); + Attrib.add_attributes + [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #> + Method.setup @{binding split} split_meth "apply case split rule"; end; diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/args.ML Fri Mar 13 23:56:07 2009 +0100 @@ -7,69 +7,66 @@ signature ARGS = sig - type T = OuterLex.token + type token = OuterLex.token type src - val src: (string * T list) * Position.T -> src - val dest_src: src -> (string * T list) * Position.T + val src: (string * token list) * Position.T -> src + val dest_src: src -> (string * token list) * Position.T val pretty_src: Proof.context -> src -> Pretty.T val map_name: (string -> string) -> src -> src val morph_values: morphism -> src -> src val maxidx_values: src -> int -> int val assignable: src -> src val closure: src -> src - val context: Context.generic * T list -> Context.proof * (Context.generic * T list) - val theory: Context.generic * T list -> Context.theory * (Context.generic * T list) - val $$$ : string -> T list -> string * T list - val add: T list -> string * T list - val del: T list -> string * T list - val colon: T list -> string * T list - val query: T list -> string * T list - val bang: T list -> string * T list - val query_colon: T list -> string * T list - val bang_colon: T list -> string * T list - val parens: (T list -> 'a * T list) -> T list -> 'a * T list - val bracks: (T list -> 'a * T list) -> T list -> 'a * T list - val mode: string -> 'a * T list -> bool * ('a * T list) - val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list - val name_source: T list -> string * T list - val name_source_position: T list -> (SymbolPos.text * Position.T) * T list - val name: T list -> string * T list - val binding: T list -> binding * T list - val alt_name: T list -> string * T list - val symbol: T list -> string * T list - val liberal_name: T list -> string * T list - val var: T list -> indexname * T list - val internal_text: T list -> string * T list - val internal_typ: T list -> typ * T list - val internal_term: T list -> term * T list - val internal_fact: T list -> thm list * T list - val internal_attribute: T list -> (morphism -> attribute) * T list - val named_text: (string -> string) -> T list -> string * T list - val named_typ: (string -> typ) -> T list -> typ * T list - val named_term: (string -> term) -> T list -> term * T list - val named_fact: (string -> thm list) -> T list -> thm list * T list - val named_attribute: (string -> morphism -> attribute) -> T list -> - (morphism -> attribute) * T list - val typ_abbrev: Context.generic * T list -> typ * (Context.generic * T list) - val typ: Context.generic * T list -> typ * (Context.generic * T list) - val term: Context.generic * T list -> term * (Context.generic * T list) - val term_abbrev: Context.generic * T list -> term * (Context.generic * T list) - val prop: Context.generic * T list -> term * (Context.generic * T list) - val tyname: Context.generic * T list -> string * (Context.generic * T list) - val const: Context.generic * T list -> string * (Context.generic * T list) - val const_proper: Context.generic * T list -> string * (Context.generic * T list) - val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list) - val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list) - -> ((int -> tactic) -> tactic) * ('a * T list) - val parse: OuterLex.token list -> T list * OuterLex.token list - val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list - val attribs: (string -> string) -> T list -> src list * T list - val opt_attribs: (string -> string) -> T list -> src list * T list - val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list - val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list - val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b - val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) -> - src -> Proof.context -> 'a * Proof.context + val context: Proof.context context_parser + val theory: theory context_parser + val $$$ : string -> string parser + val add: string parser + val del: string parser + val colon: string parser + val query: string parser + val bang: string parser + val query_colon: string parser + val bang_colon: string parser + val parens: ('a parser) -> 'a parser + val bracks: ('a parser) -> 'a parser + val mode: string -> bool context_parser + val maybe: 'a parser -> 'a option parser + val name_source: string parser + val name_source_position: (SymbolPos.text * Position.T) parser + val name: string parser + val binding: binding parser + val alt_name: string parser + val symbol: string parser + val liberal_name: string parser + val var: indexname parser + val internal_text: string parser + val internal_typ: typ parser + val internal_term: term parser + val internal_fact: thm list parser + val internal_attribute: (morphism -> attribute) parser + val named_text: (string -> string) -> string parser + val named_typ: (string -> typ) -> typ parser + val named_term: (string -> term) -> term parser + val named_fact: (string -> thm list) -> thm list parser + val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser + val typ_abbrev: typ context_parser + val typ: typ context_parser + val term: term context_parser + val term_abbrev: term context_parser + val prop: term context_parser + val tyname: string context_parser + val const: string context_parser + val const_proper: string context_parser + val bang_facts: thm list context_parser + val goal_spec: ((int -> tactic) -> tactic) context_parser + val parse: token list parser + val parse1: (string -> bool) -> token list parser + val attribs: (string -> string) -> src list parser + val opt_attribs: (string -> string) -> src list parser + val thm_name: (string -> string) -> string -> (binding * src list) parser + val opt_thm_name: (string -> string) -> string -> (binding * src list) parser + val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic + val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context end; structure Args: ARGS = @@ -78,13 +75,13 @@ structure T = OuterLex; structure P = OuterParse; +type token = T.token; + (** datatype src **) -type T = T.token; - -datatype src = Src of (string * T list) * Position.T; +datatype src = Src of (string * token list) * Position.T; val src = Src; fun dest_src (Src src) = src; @@ -236,7 +233,7 @@ $$$ "!" >> K ALLGOALS; val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]"); -fun goal_spec def = Scan.lift (Scan.optional goal def); +fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x; (* arguments within outer syntax *) diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Mar 13 23:56:07 2009 +0100 @@ -24,14 +24,13 @@ (('c * 'att list) * ('d * 'att list) list) list val crude_closure: Proof.context -> src -> src val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory - val syntax: (Context.generic * Args.T list -> - attribute * (Context.generic * Args.T list)) -> src -> attribute + val syntax: attribute context_parser -> src -> attribute val no_args: attribute -> src -> attribute val add_del_args: attribute -> attribute -> src -> attribute - val thm_sel: Args.T list -> Facts.interval list * Args.T list - val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list) - val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) - val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) + val thm_sel: Facts.interval list parser + val thm: thm context_parser + val thms: thm list context_parser + val multi_thm: thm list context_parser val print_configs: Proof.context -> unit val internal: (morphism -> attribute) -> src val register_config: Config.value Config.T -> theory -> theory diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Fri Mar 13 23:56:07 2009 +0100 @@ -615,11 +615,10 @@ default_intro_tac ctxt facts; val _ = Context.>> (Context.map_theory - (Method.add_methods - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), - "back-chain introduction rules of classes"), - ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), - "apply some intro/elim rule")])); + (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac))) + "back-chain introduction rules of classes" #> + Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) + "apply some intro/elim rule")); end; diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/code.ML Fri Mar 13 23:56:07 2009 +0100 @@ -44,7 +44,7 @@ val postprocess_conv: theory -> cterm -> thm val postprocess_term: theory -> term -> term - val add_attribute: string * (Args.T list -> attribute * Args.T list) -> theory -> theory + val add_attribute: string * attribute parser -> theory -> theory val print_codesetup: theory -> unit end; @@ -83,7 +83,7 @@ (** code attributes **) structure CodeAttr = TheoryDataFun ( - type T = (string * (Args.T list -> attribute * Args.T list)) list; + type T = (string * attribute parser) list; val empty = []; val copy = I; val extend = I; diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/element.ML Fri Mar 13 23:56:07 2009 +0100 @@ -268,7 +268,7 @@ local val refine_witness = - Proof.refine (Method.Basic (K (Method.RAW_METHOD + Proof.refine (Method.Basic (K (RAW_METHOD (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/locale.ML Fri Mar 13 23:56:07 2009 +0100 @@ -487,13 +487,10 @@ (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st; val _ = Context.>> (Context.map_theory - (Method.add_methods - [("intro_locales", - Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)), - "back-chain introduction rules of locales without unfolding predicates"), - ("unfold_locales", - Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)), - "back-chain all introduction rules of locales")])); + (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false)) + "back-chain introduction rules of locales without unfolding predicates" #> + Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true)) + "back-chain all introduction rules of locales")); end; diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/method.ML Fri Mar 13 23:56:07 2009 +0100 @@ -8,13 +8,13 @@ sig val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq - type method val trace_rules: bool ref end; signature METHOD = sig include BASIC_METHOD + type method val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method val RAW_METHOD: (thm list -> tactic) -> method @@ -78,40 +78,31 @@ -> theory -> theory val add_method: bstring * (src -> Proof.context -> method) * string -> theory -> theory + val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context + val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory val method_setup: bstring -> string * Position.T -> string -> theory -> theory - val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) - -> src -> Proof.context -> 'a * Proof.context - val simple_args: (Args.T list -> 'a * Args.T list) - -> ('a -> Proof.context -> method) -> src -> Proof.context -> method + val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method val no_args: method -> src -> Proof.context -> method type modifier - val sectioned_args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) -> - (Args.T list -> modifier * Args.T list) list -> + val sectioned_args: 'a context_parser -> modifier parser list -> ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b - val bang_sectioned_args: - (Args.T list -> modifier * Args.T list) list -> + val bang_sectioned_args: modifier parser list -> (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a - val bang_sectioned_args': - (Args.T list -> modifier * Args.T list) list -> - (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) -> + val bang_sectioned_args': modifier parser list -> 'a context_parser -> ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b - val only_sectioned_args: - (Args.T list -> modifier * Args.T list) list -> - (Proof.context -> 'a) -> src -> Proof.context -> 'a - val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> + val only_sectioned_args: modifier parser list -> (Proof.context -> 'a) -> src -> Proof.context -> 'a + val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a - val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic) - -> src -> Proof.context -> method - val goal_args': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) - -> ('a -> int -> tactic) -> src -> Proof.context -> method - val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> - (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method - val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) -> - (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method - val parse: OuterLex.token list -> text * OuterLex.token list + val goal_args: 'a parser -> ('a -> int -> tactic) -> src -> Proof.context -> method + val goal_args': 'a context_parser -> ('a -> int -> tactic) -> src -> Proof.context -> method + val goal_args_ctxt: 'a parser -> (Proof.context -> 'a -> int -> tactic) -> src -> + Proof.context -> method + val goal_args_ctxt': 'a context_parser -> (Proof.context -> 'a -> int -> tactic) -> src -> + Proof.context -> method + val parse: text parser end; structure Method: METHOD = @@ -401,7 +392,13 @@ val add_method = add_methods o Library.single; -(* method_setup *) +(* method setup *) + +fun syntax scan = Args.context_syntax "method" scan; + +fun setup name scan comment = + add_methods [(Binding.name_of name, + fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end, comment)]; fun method_setup name (txt, pos) cmt = Context.theory_map (ML_Context.expression pos @@ -418,8 +415,6 @@ (* basic *) -fun syntax scan = Args.context_syntax "method" scan; - fun simple_args scan f src ctxt : method = fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt); @@ -461,18 +456,22 @@ end; +(* extra rule methods *) + +fun xrule_meth m = + Scan.lift (Scan.optional (Args.parens OuterParse.nat) 0) -- Attrib.thms >> + (fn (n, ths) => K (m n ths)); + + (* tactic syntax *) -fun nat_thms_args f = uncurry f oo - (fst oo syntax (Scan.lift (Scan.optional (Args.parens P.nat) 0) -- Attrib.thms)); - -fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec HEADGOAL -- args >> +fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec -- args >> (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt); fun goal_args args tac = goal_args' (Scan.lift args) tac; fun goal_args_ctxt' args tac src ctxt = - fst (syntax (Args.goal_spec HEADGOAL -- args >> + fst (syntax (Args.goal_spec -- args >> (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt); fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac; @@ -505,31 +504,38 @@ (* theory setup *) val _ = Context.>> (Context.map_theory - (add_methods - [("fail", no_args fail, "force failure"), - ("succeed", no_args succeed, "succeed"), - ("-", no_args insert_facts, "do nothing (insert current facts only)"), - ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), - ("intro", thms_args intro, "repeatedly apply introduction rules"), - ("elim", thms_args elim, "repeatedly apply elimination rules"), - ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"), - ("fold", thms_ctxt_args fold_meth, "fold definitions"), - ("atomize", (atomize o fst) oo syntax (Args.mode "full"), - "present local premises as object-level statements"), - ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"), - ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), - ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), - ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), - ("this", no_args this, "apply current facts as rules"), - ("fact", thms_ctxt_args fact, "composition by facts from context"), - ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), - ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_tac, - "rename parameters of goal"), - ("rotate_tac", goal_args (Scan.optional P.int 1) Tactic.rotate_tac, - "rotate assumptions of goal"), - ("tactic", simple_args (P.position Args.name) tactic, "ML tactic as proof method"), - ("raw_tactic", simple_args (P.position Args.name) raw_tactic, - "ML tactic as raw proof method")])); + (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #> + setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #> + setup (Binding.name "-") (Scan.succeed (K insert_facts)) + "do nothing (insert current facts only)" #> + setup (Binding.name "insert") (Attrib.thms >> (K o insert)) + "insert theorems, ignoring facts (improper)" #> + setup (Binding.name "intro") (Attrib.thms >> (K o intro)) + "repeatedly apply introduction rules" #> + setup (Binding.name "elim") (Attrib.thms >> (K o elim)) + "repeatedly apply elimination rules" #> + setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #> + setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #> + setup (Binding.name "atomize") (Args.mode "full" >> (K o atomize)) + "present local premises as object-level statements" #> + setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #> + setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #> + setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #> + setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #> + setup (Binding.name "this") (Scan.succeed (K this)) "apply current facts as rules" #> + setup (Binding.name "fact") (Attrib.thms >> fact) "composition by facts from context" #> + 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)))) + "rename parameters of goal" #> + setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional P.int 1) >> + (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i)))) + "rotate assumptions of goal" #> + setup (Binding.name "tactic") (Scan.lift (P.position Args.name) >> tactic) + "ML tactic as proof method" #> + setup (Binding.name "raw_tactic") (Scan.lift (P.position Args.name) >> raw_tactic) + "ML tactic as raw proof method")); (*final declarations of this structure!*) @@ -540,3 +546,12 @@ structure BasicMethod: BASIC_METHOD = Method; open BasicMethod; + +val RAW_METHOD_CASES = Method.RAW_METHOD_CASES; +val RAW_METHOD = Method.RAW_METHOD; +val METHOD_CASES = Method.METHOD_CASES; +val METHOD = Method.METHOD; +val SIMPLE_METHOD = Method.SIMPLE_METHOD; +val SIMPLE_METHOD' = Method.SIMPLE_METHOD'; +val SIMPLE_METHOD'' = Method.SIMPLE_METHOD''; + diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/outer_parse.ML Fri Mar 13 23:56:07 2009 +0100 @@ -8,6 +8,7 @@ sig type token = OuterLex.token type 'a parser = token list -> 'a * token list + type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list) val group: string -> (token list -> 'a) -> token list -> 'a val !!! : (token list -> 'a) -> token list -> 'a val !!!! : (token list -> 'a) -> token list -> 'a @@ -50,14 +51,10 @@ val enum1: string -> 'a parser -> 'a list parser val and_list: 'a parser -> 'a list parser val and_list1: 'a parser -> 'a list parser - val enum': string -> ('a * token list -> 'b * ('a * token list)) -> - 'a * token list -> 'b list * ('a * token list) - val enum1': string -> ('a * token list -> 'b * ('a * token list)) -> - 'a * token list -> 'b list * ('a * token list) - val and_list': ('a * token list -> 'b * ('a * token list)) -> - 'a * token list -> 'b list * ('a * token list) - val and_list1': ('a * token list -> 'b * ('a * token list)) -> - 'a * token list -> 'b list * ('a * token list) + val enum': string -> 'a context_parser -> 'a list context_parser + val enum1': string -> 'a context_parser -> 'a list context_parser + val and_list': 'a context_parser -> 'a list context_parser + val and_list1': 'a context_parser -> 'a list context_parser val list: 'a parser -> 'a list parser val list1: 'a parser -> 'a list parser val name: bstring parser @@ -106,6 +103,7 @@ type token = T.token; type 'a parser = token list -> 'a * token list; +type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list); (** error handling **) @@ -339,3 +337,7 @@ val opt_target = Scan.option target; end; + +type 'a parser = 'a OuterParse.parser; +type 'a context_parser = 'a OuterParse.context_parser; + diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Fri Mar 13 23:56:07 2009 +0100 @@ -9,7 +9,6 @@ signature OUTER_SYNTAX = sig - type 'a parser = 'a OuterParse.parser val command: string -> string -> OuterKeyword.T -> (Toplevel.transition -> Toplevel.transition) parser -> unit val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/proof.ML Fri Mar 13 23:56:07 2009 +0100 @@ -780,7 +780,7 @@ in (rev vars, props') end; fun refine_terms n = - refine (Method.Basic (K (Method.RAW_METHOD + refine (Method.Basic (K (RAW_METHOD (K (HEADGOAL (PRECISE_CONJUNCTS n (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none)) #> Seq.hd; diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/rule_insts.ML --- a/src/Pure/Isar/rule_insts.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/rule_insts.ML Fri Mar 13 23:56:07 2009 +0100 @@ -386,61 +386,48 @@ local -fun gen_inst _ tac _ (quant, ([], thms)) = - Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms)) - | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) = - Method.METHOD (fn facts => - quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)) - | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules"; +fun inst_meth inst_tac tac = + Args.goal_spec -- + Scan.optional (Scan.lift + (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] -- + Attrib.thms >> + (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts => + if null insts then quant (Method.insert_tac facts THEN' tac thms) + else + (case thms of + [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm) + | _ => error "Cannot have instantiations with multiple rules"))); in -val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac; -val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac; -val cut_inst_meth = gen_inst cut_inst_tac Tactic.cut_rules_tac; -val dres_inst_meth = gen_inst dres_inst_tac Tactic.dresolve_tac; -val forw_inst_meth = gen_inst forw_inst_tac Tactic.forward_tac; +val res_inst_meth = inst_meth res_inst_tac Tactic.resolve_tac; +val eres_inst_meth = inst_meth eres_inst_tac Tactic.eresolve_tac; +val cut_inst_meth = inst_meth cut_inst_tac Tactic.cut_rules_tac; +val dres_inst_meth = inst_meth dres_inst_tac Tactic.dresolve_tac; +val forw_inst_meth = inst_meth forw_inst_tac Tactic.forward_tac; end; -(* method syntax *) - -val insts = - Scan.optional (Scan.lift - (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] - -- Attrib.thms; - -fun inst_args f src ctxt = - f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt)); - -val insts_var = - Scan.optional (Scan.lift - (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] - -- Attrib.thms; - -fun inst_args_var f src ctxt = - f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt)); - - (* setup *) val _ = Context.>> (Context.map_theory - (Method.add_methods - [("rule_tac", inst_args_var res_inst_meth, - "apply rule (dynamic instantiation)"), - ("erule_tac", inst_args_var eres_inst_meth, - "apply rule in elimination manner (dynamic instantiation)"), - ("drule_tac", inst_args_var dres_inst_meth, - "apply rule in destruct manner (dynamic instantiation)"), - ("frule_tac", inst_args_var forw_inst_meth, - "apply rule in forward manner (dynamic instantiation)"), - ("cut_tac", inst_args_var cut_inst_meth, - "cut rule (dynamic instantiation)"), - ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name_source) subgoals_tac, - "insert subgoal (dynamic instantiation)"), - ("thin_tac", Method.goal_args_ctxt Args.name_source thin_tac, - "remove premise (dynamic instantiation)")])); + (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #> + Method.setup (Binding.name "erule_tac") eres_inst_meth + "apply rule in elimination manner (dynamic instantiation)" #> + Method.setup (Binding.name "drule_tac") dres_inst_meth + "apply rule in destruct manner (dynamic instantiation)" #> + Method.setup (Binding.name "frule_tac") forw_inst_meth + "apply rule in forward manner (dynamic instantiation)" #> + Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #> + Method.setup (Binding.name "subgoal_tac") + (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >> + (fn (quant, props) => fn ctxt => SIMPLE_METHOD'' quant (subgoals_tac ctxt props))) + "insert subgoal (dynamic instantiation)" #> + Method.setup (Binding.name "thin_tac") + (Args.goal_spec -- Scan.lift Args.name_source >> + (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop))) + "remove premise (dynamic instantiation)")); end; diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/spec_parse.ML --- a/src/Pure/Isar/spec_parse.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/spec_parse.ML Fri Mar 13 23:56:07 2009 +0100 @@ -6,8 +6,6 @@ signature SPEC_PARSE = sig - type token = OuterParse.token - type 'a parser = 'a OuterParse.parser val attrib: Attrib.src parser val attribs: Attrib.src list parser val opt_attribs: Attrib.src list parser @@ -36,8 +34,6 @@ struct structure P = OuterParse; -type token = P.token; -type 'a parser = 'a P.parser; (* theorem specifications *) diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Isar/value_parse.ML --- a/src/Pure/Isar/value_parse.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Isar/value_parse.ML Fri Mar 13 23:56:07 2009 +0100 @@ -6,7 +6,6 @@ signature VALUE_PARSE = sig - type 'a parser = 'a OuterParse.parser val comma: 'a parser -> 'a parser val equal: 'a parser -> 'a parser val parens: 'a parser -> 'a parser @@ -20,7 +19,6 @@ struct structure P = OuterParse; -type 'a parser = 'a P.parser; (* syntax utilities *) diff -r c4728771f04f -r 3ec2d35b380f src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Fri Mar 13 23:56:07 2009 +0100 @@ -6,15 +6,11 @@ signature ML_ANTIQUOTE = sig - val macro: string -> - (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit + val macro: string -> Proof.context context_parser -> unit val variant: string -> Proof.context -> string * Proof.context - val inline: string -> - (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit - val declaration: string -> string -> - (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit - val value: string -> - (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit + val inline: string -> string context_parser -> unit + val declaration: string -> string -> string context_parser -> unit + val value: string -> string context_parser -> unit end; structure ML_Antiquote: ML_ANTIQUOTE = diff -r c4728771f04f -r 3ec2d35b380f src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/ML/ml_context.ML Fri Mar 13 23:56:07 2009 +0100 @@ -27,8 +27,7 @@ type antiq = {struct_name: string, background: Proof.context} -> (Proof.context -> string * string) * Proof.context - val add_antiq: string -> - (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) -> unit + val add_antiq: string -> (Position.T -> antiq context_parser) -> unit val trace: bool ref val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit val eval: bool -> Position.T -> string -> unit @@ -157,9 +156,7 @@ local -val global_parsers = ref (Symtab.empty: - (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) - Symtab.table); +val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table); in diff -r c4728771f04f -r 3ec2d35b380f src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/Thy/thy_output.ML Fri Mar 13 23:56:07 2009 +0100 @@ -18,8 +18,7 @@ val print_antiquotations: unit -> unit val boolean: string -> bool val integer: string -> int - val antiquotation: string -> - (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) -> + val antiquotation: string -> 'a context_parser -> ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit datatype markup = Markup | MarkupEnv | Verbatim val modes: string list ref diff -r c4728771f04f -r 3ec2d35b380f src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Pure/simplifier.ML Fri Mar 13 23:56:07 2009 +0100 @@ -73,11 +73,10 @@ val def_simproc_i: {name: string, lhss: term list, proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> local_theory -> local_theory - val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list - val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list - val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list - val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list - -> theory -> theory + val cong_modifiers: Method.modifier parser list + val simp_modifiers': Method.modifier parser list + val simp_modifiers: Method.modifier parser list + val method_setup: Method.modifier parser list -> theory -> theory val easy_setup: thm -> thm list -> theory -> theory end; @@ -410,11 +409,11 @@ Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers'); -fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts => +fun simp_method (prems, tac) ctxt = METHOD (fn facts => ALLGOALS (Method.insert_tac (prems @ facts)) THEN (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)); -fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts => +fun simp_method' (prems, tac) ctxt = METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' ((CHANGED_PROP) oo tac) (local_simpset_of ctxt))); diff -r c4728771f04f -r 3ec2d35b380f src/Sequents/ILL.thy --- a/src/Sequents/ILL.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Sequents/ILL.thy Fri Mar 13 23:56:07 2009 +0100 @@ -146,7 +146,7 @@ *} method_setup best_lazy = - {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *} + {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *} "lazy classical reasoning" lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B" @@ -282,10 +282,10 @@ method_setup best_safe = - {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} "" + {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} "" method_setup best_power = - {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} "" + {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} "" (* Some examples from Troelstra and van Dalen *) diff -r c4728771f04f -r 3ec2d35b380f src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Sequents/LK0.thy Fri Mar 13 23:56:07 2009 +0100 @@ -240,23 +240,23 @@ *} method_setup fast_prop = - {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *} + {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *} "propositional reasoning" method_setup fast = - {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *} + {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *} "classical reasoning" method_setup fast_dup = - {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *} + {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *} "classical reasoning" method_setup best = - {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *} + {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *} "classical reasoning" method_setup best_dup = - {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *} + {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *} "classical reasoning" diff -r c4728771f04f -r 3ec2d35b380f src/Sequents/S4.thy --- a/src/Sequents/S4.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Sequents/S4.thy Fri Mar 13 23:56:07 2009 +0100 @@ -45,7 +45,7 @@ *} method_setup S4_solve = - {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver" + {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver" (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) diff -r c4728771f04f -r 3ec2d35b380f src/Sequents/S43.thy --- a/src/Sequents/S43.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Sequents/S43.thy Fri Mar 13 23:56:07 2009 +0100 @@ -92,7 +92,7 @@ method_setup S43_solve = {* - Method.no_args (Method.SIMPLE_METHOD + Method.no_args (SIMPLE_METHOD (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)) *} "S4 solver" diff -r c4728771f04f -r 3ec2d35b380f src/Sequents/T.thy --- a/src/Sequents/T.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Sequents/T.thy Fri Mar 13 23:56:07 2009 +0100 @@ -44,7 +44,7 @@ *} method_setup T_solve = - {* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver" + {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver" (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) diff -r c4728771f04f -r 3ec2d35b380f src/Tools/atomize_elim.ML --- a/src/Tools/atomize_elim.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Tools/atomize_elim.ML Fri Mar 13 23:56:07 2009 +0100 @@ -131,9 +131,9 @@ THEN (CONVERSION (full_atomize_elim_conv ctxt) i) end) -val setup = Method.add_methods - [("atomize_elim", Method.ctxt_args (Method.SIMPLE_METHOD' o atomize_elim_tac), - "convert obtains statement to atomic object logic goal")] +val setup = + Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac)) + "convert obtains statement to atomic object logic goal" #> AtomizeElimData.setup end diff -r c4728771f04f -r 3ec2d35b380f src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Tools/code/code_target.ML Fri Mar 13 23:56:07 2009 +0100 @@ -26,7 +26,7 @@ -> (Path.T option -> 'a -> unit) -> ('a -> string * string option list) -> 'a -> serialization - val serialize: theory -> string -> string option -> Args.T list + val serialize: theory -> string -> string option -> OuterLex.token list -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization val serialize_custom: theory -> string * (serializer * literals) -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list @@ -106,7 +106,7 @@ type serializer = string option (*module name*) - -> Args.T list (*arguments*) + -> OuterLex.token list (*arguments*) -> (string -> string) (*labelled_name*) -> string list (*reserved symbols*) -> (string * Pretty.T) list (*includes*) diff -r c4728771f04f -r 3ec2d35b380f src/Tools/coherent.ML --- a/src/Tools/coherent.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Tools/coherent.ML Fri Mar 13 23:56:07 2009 +0100 @@ -225,7 +225,7 @@ end) context 1) ctxt; fun coherent_meth rules ctxt = - Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1); + METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1); val setup = Method.add_method ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula"); diff -r c4728771f04f -r 3ec2d35b380f src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Tools/eqsubst.ML Fri Mar 13 23:56:07 2009 +0100 @@ -109,8 +109,8 @@ searchinfo -> Term.term -> match Seq.seq Seq.seq (* syntax tools *) - val ith_syntax : Args.T list -> int list * Args.T list - val options_syntax : Args.T list -> bool * Args.T list + val ith_syntax : int list parser + val options_syntax : bool parser (* Isar level hooks *) val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method @@ -434,7 +434,7 @@ (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) fun eqsubst_meth ctxt occL inthms = - Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms); + SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms); (* apply a substitution inside assumption j, keeps asm in the same place *) fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) = @@ -548,7 +548,7 @@ (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) fun eqsubst_asm_meth ctxt occL inthms = - Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms); + SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms); (* syntax for options, given "(asm)" will give back true, without gives back false *) diff -r c4728771f04f -r 3ec2d35b380f src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Tools/induct.ML Fri Mar 13 23:56:07 2009 +0100 @@ -735,23 +735,22 @@ in -fun cases_meth src = - Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src - #> (fn ((insts, opt_rule), ctxt) => - Method.METHOD_CASES (fn facts => - Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))); +val cases_meth = + P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >> + (fn (insts, opt_rule) => fn ctxt => + METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))); -fun induct_meth src = - Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) -- - (arbitrary -- taking -- Scan.option induct_rule)) src - #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) => - Method.RAW_METHOD_CASES (fn facts => +val induct_meth = + P.and_list' (Scan.repeat (unless_more_args def_inst)) -- + (arbitrary -- taking -- Scan.option induct_rule) >> + (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt => + RAW_METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))); -fun coinduct_meth src = - Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src - #> (fn (((insts, taking), opt_rule), ctxt) => - Method.RAW_METHOD_CASES (fn facts => +val coinduct_meth = + Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >> + (fn ((insts, taking), opt_rule) => fn ctxt => + RAW_METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))); end; @@ -762,9 +761,8 @@ val setup = attrib_setup #> - Method.add_methods - [(casesN, cases_meth, "case analysis on types or predicates/sets"), - (inductN, induct_meth, "induction on types or predicates/sets"), - (coinductN, coinduct_meth, "coinduction on types or predicates/sets")]; + Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #> + Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #> + Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets"; end; diff -r c4728771f04f -r 3ec2d35b380f src/Tools/intuitionistic.ML --- a/src/Tools/intuitionistic.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/Tools/intuitionistic.ML Fri Mar 13 23:56:07 2009 +0100 @@ -86,7 +86,7 @@ val method = Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat)) - (fn n => fn prems => fn ctxt => Method.METHOD (fn facts => + (fn n => fn prems => fn ctxt => METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))); diff -r c4728771f04f -r 3ec2d35b380f src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/ZF/Tools/ind_cases.ML Fri Mar 13 23:56:07 2009 +0100 @@ -57,19 +57,14 @@ (* ind_cases method *) -fun mk_cases_meth (props, ctxt) = - props - |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt)) - |> Method.erule 0; - -val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source)); - - -(* package setup *) +val mk_cases_meth = Scan.lift (Scan.repeat1 Args.name_source) >> + (fn props => fn ctxt => + props + |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt)) + |> Method.erule 0); val setup = - Method.add_methods - [("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")]; + Method.setup @{binding "ind_cases"} mk_cases_meth "dynamic case analysis on sets"; (* outer syntax *) diff -r c4728771f04f -r 3ec2d35b380f src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Fri Mar 13 19:18:07 2009 +0100 +++ b/src/ZF/Tools/typechk.ML Fri Mar 13 23:56:07 2009 +0100 @@ -116,7 +116,7 @@ Method.only_sectioned_args [Args.add -- Args.colon >> K (I, TC_add), Args.del -- Args.colon >> K (I, TC_del)] - (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))); + (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))); val _ = OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag diff -r c4728771f04f -r 3ec2d35b380f src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Fri Mar 13 19:18:07 2009 +0100 +++ b/src/ZF/UNITY/Constrains.thy Fri Mar 13 23:56:07 2009 +0100 @@ -496,13 +496,11 @@ setup ProgramDefs.setup method_setup safety = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (constrains_tac ctxt)) *} + Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *} "for proving safety properties" method_setup always = {* - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (always_tac ctxt)) *} + Method.ctxt_args (SIMPLE_METHOD' o always_tac) *} "for proving invariants" end