--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Mar 17 09:34:23 2006 +0100
@@ -23,7 +23,7 @@
inv > HOL.inverse :: "real => real"
real_add > HOL.plus :: "[real,real] => real"
real_mul > HOL.times :: "[real,real] => real"
- real_lt > "op <" :: "[real,real] => bool";
+ real_lt > "Orderings.less" :: "[real,real] => bool";
ignore_thms
real_TY_DEF
@@ -51,7 +51,7 @@
const_maps
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
- real_lte > "op <=" :: "[real,real] => bool"
+ real_lte > Orderings.less_eq :: "[real,real] => bool"
real_sub > HOL.minus :: "[real,real] => real"
"/" > HOL.divide :: "[real,real] => real"
pow > Nat.power :: "[real,nat] => real"