equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 header {* Miscellaneous Datatype Definitions *} |
10 header {* Miscellaneous Datatype Definitions *} |
11 |
11 |
12 theory Misc_Datatype |
12 theory Misc_Datatype |
13 imports "../BNF" |
13 imports "~~/src/HOL/Library/More_BNFs" |
14 begin |
14 begin |
15 |
15 |
16 datatype_new simple = X1 | X2 | X3 | X4 |
16 datatype_new simple = X1 | X2 | X3 | X4 |
17 |
17 |
18 datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit |
18 datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit |