modernized method setup;
authorwenzelm
Sat May 30 12:52:57 2009 +0200 (2009-05-30)
changeset 312990c5baf034d0e
parent 31298 5e6b2b23701a
child 31300 40fa39d9bce7
modernized method setup;
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/Tools/intuitionistic.ML
     1.1 --- a/src/FOL/IFOL.thy	Sat May 30 11:57:36 2009 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sat May 30 12:52:57 2009 +0200
     1.3 @@ -610,7 +610,7 @@
     1.4  
     1.5  subsection {* Intuitionistic Reasoning *}
     1.6  
     1.7 -setup {* Intuitionistic.method_setup "iprover" *}
     1.8 +setup {* Intuitionistic.method_setup @{binding iprover} *}
     1.9  
    1.10  lemma impE':
    1.11    assumes 1: "P --> Q"
     2.1 --- a/src/HOL/HOL.thy	Sat May 30 11:57:36 2009 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat May 30 12:52:57 2009 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4    ("Tools/recfun_codegen.ML")
     2.5  begin
     2.6  
     2.7 -setup {* Intuitionistic.method_setup "iprover" *}
     2.8 +setup {* Intuitionistic.method_setup @{binding iprover} *}
     2.9  
    2.10  
    2.11  subsection {* Primitive logic *}
     3.1 --- a/src/Tools/intuitionistic.ML	Sat May 30 11:57:36 2009 +0200
     3.2 +++ b/src/Tools/intuitionistic.ML	Sat May 30 12:52:57 2009 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  signature INTUITIONISTIC =
     3.5  sig
     3.6    val prover_tac: Proof.context -> int option -> int -> tactic
     3.7 -  val method_setup: bstring -> theory -> theory
     3.8 +  val method_setup: binding -> theory -> theory
     3.9  end;
    3.10  
    3.11  structure Intuitionistic: INTUITIONISTIC =
    3.12 @@ -84,15 +84,16 @@
    3.13    modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    3.14    Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    3.15  
    3.16 -val method =
    3.17 -  Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
    3.18 -    (fn n => fn prems => fn ctxt => METHOD (fn facts =>
    3.19 -      HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    3.20 -      ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
    3.21 -
    3.22  in
    3.23  
    3.24 -fun method_setup name = Method.add_method (name, method, "intuitionistic proof search");
    3.25 +fun method_setup name =
    3.26 +  Method.setup name
    3.27 +    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
    3.28 +      Method.sections modifiers >>
    3.29 +      (fn (prems, n) => fn ctxt => METHOD (fn facts =>
    3.30 +        HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    3.31 +        ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))))
    3.32 +    "intuitionistic proof search";
    3.33  
    3.34  end;
    3.35