src/HOL/datatype.ML
changeset 3476 1be4fee7606b
parent 3308 da002cef7090
child 3534 c245c88194ff