src/HOL/Old_Datatype.thy
changeset 58366 5cf7df52d71d
parent 58305 57752a91eec4