src/HOL/Datatype.thy
changeset 24085 cbad32e7ab40
parent 22886 cdff6ef76009
child 24162 8dfd5dd65d82