src/HOL/Datatype.thy
changeset 22911 2f5e8d70a179
parent 22886 cdff6ef76009
child 24162 8dfd5dd65d82