src/HOL/Tools/typecopy.ML
changeset 37233 b78f31ca4675
parent 36610 bafd82950e24
child 37469 1436d6f28f17
equal deleted inserted replaced
37232:c10fb22a5e0c 37233:b78f31ca4675