src/HOL/Tools/typedef.ML
changeset 36551 cc42df660808
parent 36323 655e2d74de3a
child 36610 bafd82950e24