src/HOL/Hyperreal/hypreal_arith.ML
changeset 24093 5d0ecd0c8f3c
parent 24075 366d4d234814
     1.1 --- a/src/HOL/Hyperreal/hypreal_arith.ML	Tue Jul 31 19:40:23 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/hypreal_arith.ML	Tue Jul 31 19:40:24 2007 +0200
     1.3 @@ -30,14 +30,14 @@
     1.4      Simplifier.simproc (the_context ())
     1.5        "fast_hypreal_arith" 
     1.6        ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
     1.7 -    (K Fast_Arith.lin_arith_simproc);
     1.8 +    (K LinArith.lin_arith_simproc);
     1.9  
    1.10  val hypreal_arith_setup =
    1.11 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.12 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.13     {add_mono_thms = add_mono_thms,
    1.14      mult_mono_thms = mult_mono_thms,
    1.15      inj_thms = real_inj_thms @ inj_thms,
    1.16 -    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
    1.17 +    lessD = lessD,  (*Can't change lessD: the hypreals are dense!*)
    1.18      neqE = neqE,
    1.19      simpset = simpset addsimps simps}) #>
    1.20    arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>