src/HOL/arith_data.ML
changeset 18708 4b3dadb4fe33
parent 18394 fa0674cd6df1
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/arith_data.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -420,8 +420,8 @@
     1.4  in
     1.5  
     1.6  val init_lin_arith_data =
     1.7 - Fast_Arith.setup @
     1.8 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
     1.9 + Fast_Arith.setup #>
    1.10 + Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    1.11     {add_mono_thms = add_mono_thms @
    1.12      add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
    1.13      mult_mono_thms = mult_mono_thms,
    1.14 @@ -433,8 +433,9 @@
    1.15                     addsimprocs [ab_group_add_cancel.sum_conv,
    1.16                                  ab_group_add_cancel.rel_conv]
    1.17                     (*abel_cancel helps it work in abstract algebraic domains*)
    1.18 -                   addsimprocs nat_cancel_sums_add}),
    1.19 -  ArithTheoryData.init, arith_discrete "nat"];
    1.20 +                   addsimprocs nat_cancel_sums_add}) #>
    1.21 +  ArithTheoryData.init #>
    1.22 +  arith_discrete "nat";
    1.23  
    1.24  end;
    1.25  
    1.26 @@ -576,14 +577,14 @@
    1.27  (* theory setup *)
    1.28  
    1.29  val arith_setup =
    1.30 -  init_lin_arith_data @
    1.31 -  [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
    1.32 +  init_lin_arith_data #>
    1.33 +  (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
    1.34      addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
    1.35 -    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy),
    1.36 +    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #>
    1.37    Method.add_methods
    1.38      [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
    1.39 -      "decide linear arithmethic")],
    1.40 +      "decide linear arithmethic")] #>
    1.41    Attrib.add_attributes [("arith_split",
    1.42      (Attrib.no_args arith_split_add,
    1.43       Attrib.no_args Attrib.undef_local_attribute),
    1.44 -    "declaration of split rules for arithmetic procedure")]];
    1.45 +    "declaration of split rules for arithmetic procedure")];