| author | bulwahn |
| Wed May 18 15:45:33 2011 +0200 (2011-05-18) | |
| changeset 42841 | 9079f49053e5 |
| child 42857 | 1e1b74448f6b |
| permissions | -rw-r--r-- |
| 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@42841 | 13 |
(OCaml "<=") |
| 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@42841 | 20 |
(OCaml "<") |
| 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 |