| changeset 27368 | 9f90ac19e32b |
| parent 25673 | 35a6c1b1c8e3 |
| child 27487 | c8a6ce181805 |
| 27367:a75d71c73362 | 27368:9f90ac19e32b |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Monolithic strings (message strings) for code generation *} |
5 header {* Monolithic strings (message strings) for code generation *} |
6 |
6 |
7 theory Code_Message |
7 theory Code_Message |
8 imports List |
8 imports Plain List |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Datatype of messages *} |
11 subsection {* Datatype of messages *} |
12 |
12 |
13 datatype message_string = STR string |
13 datatype message_string = STR string |