| author | blanchet |
| Wed, 12 Dec 2012 03:47:02 +0100 | |
| changeset 50486 | d5dc28fafd9d |
| parent 42857 | 1e1b74448f6b |
| permissions | -rw-r--r-- |
|
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) <= _)") |
|
42857
1e1b74448f6b
a deeper understanding of the code generation adaptation compared to 9079f49053e5
bulwahn
parents:
42841
diff
changeset
|
13 |
(OCaml "!((_ : char) <= _)") |
|
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
|
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) < _)") |
|
42857
1e1b74448f6b
a deeper understanding of the code generation adaptation compared to 9079f49053e5
bulwahn
parents:
42841
diff
changeset
|
20 |
(OCaml "!((_ : char) < _)") |
|
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
|
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 |