src/HOL/Import/Generate-HOL/GenHOL4Real.thy

   real_1   > 1           :: real
   real_neg > uminus      :: "real => real"
   inv      > HOL.inverse :: "real => real"
   real_add > HOL.plus    :: "[real,real] => real"
   real_mul > HOL.times   :: "[real,real] => real"
-  real_lt  > Orderings.ord_class.less :: "[real,real] => bool";
+  real_lt  > HOL.ord_class.less :: "[real,real] => bool";
 
 ignore_thms
     real_TY_DEF
     real_tybij
     real_0

 import_theory real;
 
 const_maps
   real_gt     > HOL4Compat.real_gt
   real_ge     > HOL4Compat.real_ge
-  real_lte    > Orderings.ord_class.less_eq :: "[real,real] => bool"
+  real_lte    > HOL.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"
   abs         > HOL.abs      :: "real => real"
   real_of_num > RealDef.real :: "nat => real";