src/HOL/Datatype.thy
changeset 33689 d0a9ce721e0c
parent 33633 9f7280e0c231
child 33959 2afc55e8ed27