src/HOL/Tools/typedef.ML
changeset 35280 54ab4921f826
parent 35238 18ae6ef02fe0
child 35351 7425aece4ee3