--- a/src/HOL/NSA/HyperDef.thy Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/NSA/HyperDef.thy Wed Jun 29 18:12:34 2011 +0200
@@ -348,12 +348,12 @@
#> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
@{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
@{thm star_of_diff}, @{thm star_of_mult}]
- #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
- #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc_global @{theory}
- "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- (K Lin_Arith.simproc)]))
+ #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
*}
+simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
+ {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+
subsection {* Exponentials on the Hyperreals *}