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