src/HOL/Datatype.thy
changeset 39214 49fc6c842d6c
parent 39198 f967a16dfcdd
child 39302 d7728f65b353