--- a/src/HOL/Real/rat_arith.ML Wed May 23 02:33:42 2007 +0200
+++ b/src/HOL/Real/rat_arith.ML Wed May 23 02:50:19 2007 +0200
@@ -32,10 +32,6 @@
in
-val fast_rat_arith_simproc = Simplifier.simproc @{theory}
- "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
- Fast_Arith.lin_arith_prover
-
val ratT = Type ("Rational.rat", [])
val rat_arith_setup =
--- a/src/HOL/Real/real_arith.ML Wed May 23 02:33:42 2007 +0200
+++ b/src/HOL/Real/real_arith.ML Wed May 23 02:50:19 2007 +0200
@@ -28,11 +28,6 @@
in
-val fast_real_arith_simproc =
- Simplifier.simproc (the_context ())
- "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"]
- Fast_Arith.lin_arith_prover;
-
val real_arith_setup =
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,