# HG changeset patch
# User huffman
# Date 1179881419 -7200
# Node ID 636cda81978aa87c2dfe4507587da9e29fe38913
# Parent  2f8d7aa1263b88aa463bc35c2dfecb10e2d4e54d
remove unused simproc definition

diff -r 2f8d7aa1263b -r 636cda81978a src/HOL/Real/rat_arith.ML
--- 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 =
diff -r 2f8d7aa1263b -r 636cda81978a src/HOL/Real/real_arith.ML
--- 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,