src/HOL/Datatype.thy
changeset 22330 00ca68f5ce29
parent 22230 bdec4a82f385
child 22424 8a5412121687