src/HOL/datatype.ML
changeset 3362 0b268cff9344
parent 3308 da002cef7090
child 3534 c245c88194ff