src/HOL/typedef.ML
changeset 3942 1f1c1f524d19
parent 3793 6e807b50b6c1
child 3946 34152864655c
equal deleted inserted replaced
3941:ea440c63d206 3942:1f1c1f524d19