src/HOL/Library/Code_Char_ord.thy
author Christian Sternagel
Wed Aug 29 12:23:14 2012 +0900 (2012-08-29)
changeset 49083 01081bca31b6
parent 42857 1e1b74448f6b
permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
     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