src/HOL/Datatype.thy
changeset 27125 0733f575b51e
parent 27104 791607529f6d
child 27823 52971512d1a2