changeset 23081 | 636cda81978a |
parent 23079 | 044a1bd3bb2a |
child 23346 | 1517207ec8b9 |
--- 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 =