src/HOL/Library/Code_Char_ord.thy
changeset 42857 1e1b74448f6b
parent 42841 9079f49053e5
--- a/src/HOL/Library/Code_Char_ord.thy	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Library/Code_Char_ord.thy	Thu May 19 18:09:20 2011 +0200
@@ -10,14 +10,14 @@
   
 code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) <= _)")
-  (OCaml "<=")
+  (OCaml "!((_ : char) <= _)")
   (Haskell infix 4 "<=")
   (Scala infixl 4 "<=")
   (Eval infixl 6 "<=")
 
 code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) < _)")
-  (OCaml "<")
+  (OCaml "!((_ : char) < _)")
   (Haskell infix 4 "<")
   (Scala infixl 4 "<")
   (Eval infixl 6 "<")