src/HOL/Library/Code_Char_ord.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 42857 1e1b74448f6b
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/Code_Char_ord.thy
     2     Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
     3 *)
     4 
     5 header {* Code generation of orderings for pretty characters *}
     6 
     7 theory Code_Char_ord
     8 imports Code_Char Char_ord
     9 begin
    10   
    11 code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    12   (SML "!((_ : char) <= _)")
    13   (OCaml "!((_ : char) <= _)")
    14   (Haskell infix 4 "<=")
    15   (Scala infixl 4 "<=")
    16   (Eval infixl 6 "<=")
    17 
    18 code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    19   (SML "!((_ : char) < _)")
    20   (OCaml "!((_ : char) < _)")
    21   (Haskell infix 4 "<")
    22   (Scala infixl 4 "<")
    23   (Eval infixl 6 "<")
    24 
    25 end