src/HOL/Datatype.thy
changeset 20719 bf00c5935432
parent 20588 c847c56edf0c
child 20798 3275b03e2fff