changeset 30663 | 0b6aff7451b2 |
parent 30007 | 74d83bd18977 |
child 31046 | c1969f609bf7 |
30662:396be15b95d5 | 30663:0b6aff7451b2 |
---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Code generation of pretty characters (and strings) *} |
5 header {* Code generation of pretty characters (and strings) *} |
6 |
6 |
7 theory Code_Char |
7 theory Code_Char |
8 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval" |
8 imports List Code_Eval Main |
9 begin |
9 begin |
10 |
10 |
11 code_type char |
11 code_type char |
12 (SML "char") |
12 (SML "char") |
13 (OCaml "char") |
13 (OCaml "char") |