--- a/src/HOL/Orderings.thy Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Orderings.thy Tue Jan 17 16:36:57 2006 +0100
@@ -703,4 +703,10 @@
leave out the "(xtrans)" above.
*)
+subsection {* Code generator setup *}
+
+code_alias
+ "op <=" "Orderings.op_le"
+ "op <" "Orderings.op_lt"
+
end