src/HOL/Library/Code_Char_ord.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 42857 1e1b74448f6b
permissions -rw-r--r--
Quotient_Info stores only relation maps
bulwahn@42841
     1
(*  Title:      HOL/Library/Code_Char_ord.thy
bulwahn@42841
     2
    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
bulwahn@42841
     3
*)
bulwahn@42841
     4
bulwahn@42841
     5
header {* Code generation of orderings for pretty characters *}
bulwahn@42841
     6
bulwahn@42841
     7
theory Code_Char_ord
bulwahn@42841
     8
imports Code_Char Char_ord
bulwahn@42841
     9
begin
bulwahn@42841
    10
  
bulwahn@42841
    11
code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
bulwahn@42841
    12
  (SML "!((_ : char) <= _)")
bulwahn@42857
    13
  (OCaml "!((_ : char) <= _)")
bulwahn@42841
    14
  (Haskell infix 4 "<=")
bulwahn@42841
    15
  (Scala infixl 4 "<=")
bulwahn@42841
    16
  (Eval infixl 6 "<=")
bulwahn@42841
    17
bulwahn@42841
    18
code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
bulwahn@42841
    19
  (SML "!((_ : char) < _)")
bulwahn@42857
    20
  (OCaml "!((_ : char) < _)")
bulwahn@42841
    21
  (Haskell infix 4 "<")
bulwahn@42841
    22
  (Scala infixl 4 "<")
bulwahn@42841
    23
  (Eval infixl 6 "<")
bulwahn@42841
    24
bulwahn@42841
    25
end