equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 section \<open>Miscellaneous Codatatype Definitions\<close> |
10 section \<open>Miscellaneous Codatatype Definitions\<close> |
11 |
11 |
12 theory Misc_Codatatype |
12 theory Misc_Codatatype |
13 imports "~~/src/HOL/Library/FSet" |
13 imports "HOL-Library.FSet" |
14 begin |
14 begin |
15 |
15 |
16 codatatype simple = X1 | X2 | X3 | X4 |
16 codatatype simple = X1 | X2 | X3 | X4 |
17 |
17 |
18 codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit |
18 codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit |