src/HOL/Datatype.thy
changeset 5330 8c9fadda81f4
parent 5181 4ba3787d9709
child 5714 b4f2e281a907