src/HOL/Datatype.thy
changeset 27756 24d0e890b432
parent 27104 791607529f6d
child 27823 52971512d1a2