| changeset 27368 | 9f90ac19e32b |
| parent 25965 | 05df64f786a4 |
| child 27487 | c8a6ce181805 |
| 27367:a75d71c73362 | 27368:9f90ac19e32b |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Code generation of pretty characters (and strings) *} |
6 header {* Code generation of pretty characters (and strings) *} |
7 |
7 |
8 theory Code_Char |
8 theory Code_Char |
9 imports List |
9 imports Plain List |
10 begin |
10 begin |
11 |
11 |
12 declare char.recs [code func del] char.cases [code func del] |
12 declare char.recs [code func del] char.cases [code func del] |
13 |
13 |
14 lemma [code func]: |
14 lemma [code func]: |