changeset 19277 | f7602e74d948 |
parent 19233 | 77ca20b0ed77 |
child 22997 | d4f3b015b50b |
--- a/src/HOL/Import/HOL/real.imp Thu Mar 16 20:19:25 2006 +0100 +++ b/src/HOL/Import/HOL/real.imp Fri Mar 17 09:34:23 2006 +0100 @@ -12,7 +12,7 @@ "sum" > "HOL4Real.real.sum" "real_sub" > "HOL.minus" :: "real => real => real" "real_of_num" > "RealDef.real" :: "nat => real" - "real_lte" > "op <=" :: "real => real => bool" + "real_lte" > "Orderings.less_eq" :: "real => real => bool" "real_gt" > "HOL4Compat.real_gt" "real_ge" > "HOL4Compat.real_ge" "pow" > "Nat.power" :: "real => nat => real"