src/HOL/datatype.ML
changeset 2981 aa5aeb6467c6
parent 2880 a0fde30aa126
child 3040 7d48671753da