src/HOL/Tools/typecopy.ML
changeset 32610 c477b0a62ce9
parent 32378 89b19ab3b35c
child 33314 53d49370f7af
equal deleted inserted replaced
32608:c0056c2c1d17 32610:c477b0a62ce9