src/HOL/int_arith1.ML
changeset 24093 5d0ecd0c8f3c
parent 24075 366d4d234814
child 24196 f1dbfd7e3223
--- a/src/HOL/int_arith1.ML	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/int_arith1.ML	Tue Jul 31 19:40:24 2007 +0200
@@ -591,7 +591,7 @@
 in
 
 val int_arith_setup =
-  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
     inj_thms = nat_inj_thms @ inj_thms,
@@ -610,6 +610,6 @@
   "fast_int_arith" 
      ["(m::'a::{ordered_idom,number_ring}) < n",
       "(m::'a::{ordered_idom,number_ring}) <= n",
-      "(m::'a::{ordered_idom,number_ring}) = n"] (K Fast_Arith.lin_arith_simproc);
+      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
 
 Addsimprocs [fast_int_arith_simproc];