src/HOL/Library/Code_Char_ord.thy
author bulwahn
Wed, 18 May 2011 15:45:33 +0200
changeset 42841 9079f49053e5
child 42857 1e1b74448f6b
permissions -rw-r--r--
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42841
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     1
(*  Title:      HOL/Library/Code_Char_ord.thy
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     2
    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     3
*)
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     4
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     5
header {* Code generation of orderings for pretty characters *}
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     6
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     7
theory Code_Char_ord
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     8
imports Code_Char Char_ord
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
     9
begin
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    10
  
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    11
code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    12
  (SML "!((_ : char) <= _)")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    13
  (OCaml "<=")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    14
  (Haskell infix 4 "<=")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    15
  (Scala infixl 4 "<=")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    16
  (Eval infixl 6 "<=")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    17
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    18
code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    19
  (SML "!((_ : char) < _)")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    20
  (OCaml "<")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    21
  (Haskell infix 4 "<")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    22
  (Scala infixl 4 "<")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    23
  (Eval infixl 6 "<")
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    24
9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
diff changeset
    25
end