| changeset 30007 | 74d83bd18977 |
| parent 28346 | b8390cd56b8f |
| child 30663 | 0b6aff7451b2 |
| 30006:f54b48cda286 | 30007:74d83bd18977 |
|---|---|
1 (* Title: HOL/Library/Code_Char.thy |
1 (* Title: HOL/Library/Code_Char.thy |
2 ID: $Id$ |
|
3 Author: Florian Haftmann |
2 Author: Florian Haftmann |
4 *) |
3 *) |
5 |
4 |
6 header {* Code generation of pretty characters (and strings) *} |
5 header {* Code generation of pretty characters (and strings) *} |
7 |
6 |