src/HOL/Datatype_Examples/Misc_Datatype.thy
changeset 58889 5b7a9633cfa8
parent 58455 126c353540fc
child 58966 0297e1277ed2
equal deleted inserted replaced
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