src/HOL/Datatype.thy
changeset 5526 e7617b57a3e6
parent 5181 4ba3787d9709
child 5714 b4f2e281a907