equal
deleted
inserted
replaced
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 List |
10 begin |
10 begin |
|
11 |
|
12 declare char.recs [code func del] char.cases [code func del] |
|
13 |
|
14 lemma [code func]: |
|
15 "size (c\<Colon>char) = 0" |
|
16 by (cases c) simp |
|
17 |
|
18 lemma [code func]: |
|
19 "char_size (c\<Colon>char) = 0" |
|
20 by (cases c) simp |
11 |
21 |
12 code_type char |
22 code_type char |
13 (SML "char") |
23 (SML "char") |
14 (OCaml "char") |
24 (OCaml "char") |
15 (Haskell "Char") |
25 (Haskell "Char") |