src/HOL/int_arith1.ML
changeset 24093 5d0ecd0c8f3c
parent 24075 366d4d234814
child 24196 f1dbfd7e3223
     1.1 --- a/src/HOL/int_arith1.ML	Tue Jul 31 19:40:23 2007 +0200
     1.2 +++ b/src/HOL/int_arith1.ML	Tue Jul 31 19:40:24 2007 +0200
     1.3 @@ -591,7 +591,7 @@
     1.4  in
     1.5  
     1.6  val int_arith_setup =
     1.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.8 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.9     {add_mono_thms = add_mono_thms,
    1.10      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
    1.11      inj_thms = nat_inj_thms @ inj_thms,
    1.12 @@ -610,6 +610,6 @@
    1.13    "fast_int_arith" 
    1.14       ["(m::'a::{ordered_idom,number_ring}) < n",
    1.15        "(m::'a::{ordered_idom,number_ring}) <= n",
    1.16 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K Fast_Arith.lin_arith_simproc);
    1.17 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
    1.18  
    1.19  Addsimprocs [fast_int_arith_simproc];