src/HOL/Tools/Presburger/presburger.ML
changeset 18708 4b3dadb4fe33
parent 18393 af72cbfa00a5
child 19233 77ca20b0ed77
     1.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  sig
     1.5   val presburger_tac : bool -> bool -> int -> tactic
     1.6   val presburger_method : bool -> bool -> int -> Proof.method
     1.7 - val setup : (theory -> theory) list
     1.8 + val setup : theory -> theory
     1.9   val trace : bool ref
    1.10  end;
    1.11  
    1.12 @@ -364,12 +364,12 @@
    1.13    Method.insert_tac facts 1 THEN presburger_tac q a i)
    1.14  
    1.15  val setup =
    1.16 -  [Method.add_method ("presburger",
    1.17 -     presburger_args presburger_method,
    1.18 -     "decision procedure for Presburger arithmetic"),
    1.19 -   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
    1.20 -     {splits = splits, inj_consts = inj_consts, discrete = discrete,
    1.21 -      presburger = SOME (presburger_tac true true)})];
    1.22 +  Method.add_method ("presburger",
    1.23 +    presburger_args presburger_method,
    1.24 +    "decision procedure for Presburger arithmetic") #>
    1.25 +  ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
    1.26 +    {splits = splits, inj_consts = inj_consts, discrete = discrete,
    1.27 +      presburger = SOME (presburger_tac true true)});
    1.28  
    1.29  end;
    1.30