src/HOL/Datatype.thy
changeset 22905 dab6a898b47c
parent 22886 cdff6ef76009
child 24162 8dfd5dd65d82