changeset 15186 | 1fb9a1fe8d0c |
parent 15184 | d2c19aea17bc |
child 15531 | 08c8dad8e399 |
--- a/src/HOL/Real/real_arith.ML Tue Sep 07 11:42:50 2004 +0200 +++ b/src/HOL/Real/real_arith.ML Tue Sep 07 13:41:30 2004 +0200 @@ -126,7 +126,6 @@ simpset = simpset addsimps simps}), arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT), arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT), - arith_discrete ("RealDef.real",false), Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]]; (* some thms for injection nat => real: