src/HOL/Datatype.thy
changeset 27514 6fcf6864d703
parent 27104 791607529f6d
child 27823 52971512d1a2