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

 end_import;
 
 import_theory prim_rec;
 
 const_maps
-    "<" > Algebras.less :: "[nat,nat]=>bool";
+    "<" > Orderings.less :: "[nat,nat]=>bool";
 
 end_import;
 
 import_theory arithmetic;
 

   NUMERAL      > HOL4Compat.NUMERAL
   num_case     > Nat.nat.nat_case
   ">"          > HOL4Compat.nat_gt
   ">="         > HOL4Compat.nat_ge
   FUNPOW       > HOL4Compat.FUNPOW
-  "<="         > Algebras.less_eq :: "[nat,nat]=>bool"
+  "<="         > Orderings.less_eq :: "[nat,nat]=>bool"
   "+"          > Algebras.plus :: "[nat,nat]=>nat"
   "*"          > Algebras.times :: "[nat,nat]=>nat"
   "-"          > Algebras.minus :: "[nat,nat]=>nat"
   MIN          > Orderings.min :: "[nat,nat]=>nat"
   MAX          > Orderings.max :: "[nat,nat]=>nat"