src/HOL/Tools/typecopy.ML
changeset 33978 2380c1dac86e
parent 33553 35f2b30593a8
child 35743 c506c029a082
equal deleted inserted replaced
33977:406d8e34a3cf 33978:2380c1dac86e