| author | himmelma |
| Thu, 28 May 2009 18:59:51 +0200 | |
| changeset 31283 | 86093a969bcd |
| parent 31053 | b7e1c065b6e4 |
| child 32657 | 5f13912245ff |
| permissions | -rw-r--r-- |
| 24999 | 1 |
(* Title: HOL/Library/Code_Char.thy |
2 |
Author: Florian Haftmann |
|
3 |
*) |
|
4 |
||
5 |
header {* Code generation of pretty characters (and strings) *}
|
|
6 |
||
7 |
theory Code_Char |
|
|
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
30007
diff
changeset
|
8 |
imports List Code_Eval Main |
| 24999 | 9 |
begin |
10 |
||
11 |
code_type char |
|
12 |
(SML "char") |
|
13 |
(OCaml "char") |
|
14 |
(Haskell "Char") |
|
15 |
||
16 |
setup {*
|
|
| 31053 | 17 |
fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] |
18 |
#> String_Code.add_literal_list_string "Haskell" |
|
| 24999 | 19 |
*} |
20 |
||
21 |
code_instance char :: eq |
|
22 |
(Haskell -) |
|
23 |
||
24 |
code_reserved SML |
|
25 |
char |
|
26 |
||
27 |
code_reserved OCaml |
|
28 |
char |
|
29 |
||
|
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28244
diff
changeset
|
30 |
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
| 24999 | 31 |
(SML "!((_ : char) = _)") |
32 |
(OCaml "!((_ : char) = _)") |
|
33 |
(Haskell infixl 4 "==") |
|
34 |
||
| 28228 | 35 |
code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term" |
| 31046 | 36 |
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
| 28228 | 37 |
|
| 24999 | 38 |
end |