bulwahn@42841: (*  Title:      HOL/Library/Code_Char_ord.thy
bulwahn@42841:     Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
bulwahn@42841: *)
bulwahn@42841: 
bulwahn@42841: header {* Code generation of orderings for pretty characters *}
bulwahn@42841: 
bulwahn@42841: theory Code_Char_ord
bulwahn@42841: imports Code_Char Char_ord
bulwahn@42841: begin
bulwahn@42841:   
bulwahn@42841: code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
bulwahn@42841:   (SML "!((_ : char) <= _)")
bulwahn@42857:   (OCaml "!((_ : char) <= _)")
bulwahn@42841:   (Haskell infix 4 "<=")
bulwahn@42841:   (Scala infixl 4 "<=")
bulwahn@42841:   (Eval infixl 6 "<=")
bulwahn@42841: 
bulwahn@42841: code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
bulwahn@42841:   (SML "!((_ : char) < _)")
bulwahn@42857:   (OCaml "!((_ : char) < _)")
bulwahn@42841:   (Haskell infix 4 "<")
bulwahn@42841:   (Scala infixl 4 "<")
bulwahn@42841:   (Eval infixl 6 "<")
bulwahn@42841: 
bulwahn@42841: end