Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
a deeper understanding of the code generation adaptation compared to 9079f49053e5
authorbulwahn
Thu, 19 May 2011 18:09:20 +0200
changeset 42857 1e1b74448f6b
parent 42856 9eef1dc200a8
child 42858 348fa5df7d3f
a deeper understanding of the code generation adaptation compared to 9079f49053e5
src/HOL/Library/Code_Char_ord.thy file | annotate | diff | comparison | revisions 
--- 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 "<")
isabelle