--- a/src/HOL/Real/Float.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Real/Float.ML Fri Mar 17 09:34:23 2006 +0100
@@ -335,12 +335,12 @@
val float_mult_const = Const ("HOL.times", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
val float_uminus_const = Const ("HOL.uminus", HOLogic.realT --> HOLogic.realT)
val float_abs_const = Const ("HOL.abs", HOLogic.realT --> HOLogic.realT)
-val float_le_const = Const ("op <=", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT)
+val float_le_const = Const ("Orderings.less_eq", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT)
val float_pprt_const = Const ("OrderedGroup.pprt", HOLogic.realT --> HOLogic.realT)
val float_nprt_const = Const ("OrderedGroup.nprt", HOLogic.realT --> HOLogic.realT)
-val nat_le_const = Const ("op <=", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-val nat_less_const = Const ("op <", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val nat_le_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val nat_less_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val nat_eq_const = Const ("op =", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val zero = FloatArith.izero