ExHOL_DatatypeMutuallyRecursive.thy revision 4d4ee5ef6601170c9d419da9fe8742c506507d11
theory ExHOL_DatatypeMutuallyRecursive
imports Datatype
begin
datatype (type4) type1 =
foo |
bar type2
and type2 = "nat * type1"
and type3 = "nat * type2"
end