src/HOL/Datatype.thy
changeset 22172 e7d6cb237b5e
parent 21905 500f91bf992c
child 22230 bdec4a82f385