src/Tools/subtyping.ML
changeset 67921 1722384ffd4a
parent 67149 e61557884799
child 74561 8e6c973003c8
equal deleted inserted replaced
67920:c3c74310154e 67921:1722384ffd4a