src/HOL/Old_Datatype.thy
changeset 58223 ba7a2d19880c
parent 58182 82478e6c60cb
child 58305 57752a91eec4