src/Pure/unify.ML
changeset 77617 58b7f3fb73cb
parent 69575 f77cc54f6d47
child 78652 3c57995c255c
equal deleted inserted replaced
77616:29effd67d8a8 77617:58b7f3fb73cb