src/HOL/typedef.ML
changeset 3362 0b268cff9344
parent 2934 bd922fc9001b
child 3768 67f4ac759100