src/HOL/datatype.ML
changeset 2056 93c093620c28
parent 2031 03a843f0f447
child 2270 d7513875b2b8
equal deleted inserted replaced
2055:cc274e47f607 2056:93c093620c28