src/HOL/NSA/HyperDef.thy
changeset 31101 26c7bb764a38
parent 31100 6a2e67fe4488
child 35028 108662d50512
     1.1 --- a/src/HOL/NSA/HyperDef.thy	Mon May 11 15:18:32 2009 +0200
     1.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon May 11 15:57:29 2009 +0200
     1.3 @@ -351,7 +351,7 @@
     1.4    #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
     1.5    #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
     1.6        "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
     1.7 -      (K Lin_Arith.lin_arith_simproc)]))
     1.8 +      (K Lin_Arith.simproc)]))
     1.9  *}
    1.10  
    1.11