src/HOL/typedef.ML
changeset 3895 b2463861c86a
parent 3793 6e807b50b6c1
child 3946 34152864655c