src/HOL/datatype.ML
changeset 4625 9c6082518cfb
parent 4613 67a726003cf8
child 4874 c66a42846887