src/HOL/arith_data.ML
changeset 17875 d81094515061
parent 17611 61556de6ef46
child 17951 ff954cc338c7
     1.1 --- a/src/HOL/arith_data.ML	Mon Oct 17 19:19:29 2005 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Mon Oct 17 23:10:10 2005 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  (* rewriting *)
     1.5  
     1.6  fun simp_all_tac rules ss =
     1.7 -  ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rules));
     1.8 +  ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules));
     1.9  
    1.10  val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    1.11  val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    1.12 @@ -394,7 +394,7 @@
    1.13  val add_rules =
    1.14   [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
    1.15    One_nat_def,isolateSuc,
    1.16 -  order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, 
    1.17 +  order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
    1.18    zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
    1.19  
    1.20  val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
    1.21 @@ -431,7 +431,7 @@
    1.22      neqE = [linorder_neqE_nat,
    1.23        get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
    1.24      simpset = HOL_basic_ss addsimps add_rules
    1.25 -                   addsimprocs [ab_group_add_cancel.sum_conv, 
    1.26 +                   addsimprocs [ab_group_add_cancel.sum_conv,
    1.27                                  ab_group_add_cancel.rel_conv]
    1.28                     (*abel_cancel helps it work in abstract algebraic domains*)
    1.29                     addsimprocs nat_cancel_sums_add}),
    1.30 @@ -538,15 +538,14 @@
    1.31  (* theory setup *)
    1.32  
    1.33  val arith_setup =
    1.34 - [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
    1.35    init_lin_arith_data @
    1.36 -  [Simplifier.change_simpset_of (op addSolver)
    1.37 -   (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac),
    1.38 -  Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
    1.39 +  [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
    1.40 +    addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
    1.41 +    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy),
    1.42    Method.add_methods
    1.43 -      [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
    1.44 -	"decide linear arithmethic")],
    1.45 +    [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
    1.46 +      "decide linear arithmethic")],
    1.47    Attrib.add_attributes [("arith_split",
    1.48 -    (Attrib.no_args arith_split_add, 
    1.49 +    (Attrib.no_args arith_split_add,
    1.50       Attrib.no_args Attrib.undef_local_attribute),
    1.51      "declaration of split rules for arithmetic procedure")]];