src/HOL/Datatype.thy
changeset 29380 a9ee3475abf4
parent 29183 f1648e009dc1
child 29580 117b88da143c