src/HOL/datatype.ML
changeset 2187 07c471510cf1
parent 2031 03a843f0f447
child 2270 d7513875b2b8