changeset 58889 | 5b7a9633cfa8 |
parent 58455 | 126c353540fc |
child 63167 | 0909deb8059b |
--- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy Sun Nov 02 18:21:14 2014 +0100 +++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy Sun Nov 02 18:21:45 2014 +0100 @@ -7,7 +7,7 @@ Miscellaneous codatatype definitions. *) -header {* Miscellaneous Codatatype Definitions *} +section {* Miscellaneous Codatatype Definitions *} theory Misc_Codatatype imports "~~/src/HOL/Library/FSet"