changeset 58889 | 5b7a9633cfa8 |
parent 58455 | 126c353540fc |
child 58966 | 0297e1277ed2 |
58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
---|---|
5 Copyright 2012, 2013 |
5 Copyright 2012, 2013 |
6 |
6 |
7 Miscellaneous datatype definitions. |
7 Miscellaneous datatype definitions. |
8 *) |
8 *) |
9 |
9 |
10 header {* Miscellaneous Datatype Definitions *} |
10 section {* Miscellaneous Datatype Definitions *} |
11 |
11 |
12 theory Misc_Datatype |
12 theory Misc_Datatype |
13 imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet" |
13 imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet" |
14 begin |
14 begin |
15 |
15 |