src/HOL/datatype.ML
changeset 2651 60d8d06f84a5
parent 2270 d7513875b2b8
child 2880 a0fde30aa126