src/HOL/datatype.ML
changeset 3339 cfa72a70f2b5
parent 3308 da002cef7090
child 3534 c245c88194ff