--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Thu May 17 19:49:40 2007 +0200
@@ -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 > "Orderings.less" :: "[real,real] => bool";
+ real_lt > Orderings.ord_class.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 > Orderings.less_eq :: "[real,real] => bool"
+ real_lte > Orderings.ord_class.less_eq :: "[real,real] => bool"
real_sub > HOL.minus :: "[real,real] => real"
"/" > HOL.divide :: "[real,real] => real"
pow > Nat.power :: "[real,nat] => real"