src/HOL/datatype.ML
changeset 2355 ee9bdbe2ac8a
parent 2270 d7513875b2b8
child 2880 a0fde30aa126