| changeset 52280 | 0a2371e7ced3 |
| parent 49446 | 6efff142bb54 |
| 52279:ac9e909fe55d | 52280:0a2371e7ced3 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Code generation of pretty characters with character codes *} |
5 header {* Code generation of pretty characters with character codes *} |
6 |
6 |
7 theory Code_Char_chr |
7 theory Code_Char_chr |
8 imports Char_nat Code_Char Code_Integer Main |
8 imports Char_nat Code_Char Code_Target_Int Main |
9 begin |
9 begin |
10 |
10 |
11 definition |
11 definition |
12 "int_of_char = int o nat_of_char" |
12 "int_of_char = int o nat_of_char" |
13 |
13 |