src/HOL/Tools/typecopy.ML
changeset 36046 c3946372f556
parent 35994 9cc3df9a606e
child 36150 123f721c9a37
equal deleted inserted replaced
36045:b846881928ea 36046:c3946372f556