src/HOL/Library/Code_Char_ord.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Char_ord.thy	Wed May 18 15:45:33 2011 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/Library/Code_Char_ord.thy
+    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
+*)
+
+header {* Code generation of orderings for pretty characters *}
+
+theory Code_Char_ord
+imports Code_Char Char_ord
+begin
+  
+code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) <= _)")
+  (OCaml "<=")
+  (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
+  (Eval infixl 6 "<=")
+
+code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) < _)")
+  (OCaml "<")
+  (Haskell infix 4 "<")
+  (Scala infixl 4 "<")
+  (Eval infixl 6 "<")
+
+end
\ No newline at end of file