src/HOL/Library/Code_Char_ord.thy
author Christian Sternagel
Thu Dec 13 13:11:38 2012 +0100 (2012-12-13)
changeset 50516 ed6b40d15d1c
parent 42857 1e1b74448f6b
permissions -rw-r--r--
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
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