| changeset 20807 | bd3b60f9a343 |
| parent 20713 | 823967ef47f1 |
| child 20936 | dc5dc0e55938 |
| 20806:3728dba101f1 | 20807:bd3b60f9a343 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Test and Examples for code generator *} |
5 header {* Test and Examples for code generator *} |
6 |
6 |
7 theory Codegenerator |
7 theory Codegenerator |
8 imports Main "~~/src/HOL/ex/Records" |
8 imports Main Records |
9 begin |
9 begin |
10 |
10 |
11 subsection {* booleans *} |
11 subsection {* booleans *} |
12 |
12 |
13 definition |
13 definition |