diff -r a2eeeb335a48 -r 368c70ee1f46 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Wed Nov 20 11:12:35 2013 +0100
+++ b/src/HOL/Library/Code_Char.thy	Wed Nov 20 11:59:33 2013 +0100
@@ -97,6 +97,18 @@
     and (Haskell) infix 4 "<"
     and (Scala) infixl 4 "<"
     and (Eval) infixl 6 "<"
+|  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+    (SML) "!((_ : string) <= _)"
+    and (OCaml) "!((_ : string) <= _)"
+    and (Haskell) infix 4 "<="
+    and (Scala) infixl 4 "<="
+    and (Eval) infixl 6 "<="
+| constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+    (SML) "!((_ : string) < _)"
+    and (OCaml) "!((_ : string) < _)"
+    and (Haskell) infix 4 "<"
+    and (Scala) infixl 4 "<"
+    and (Eval) infixl 6 "<"
 
 end