src/Pure/unify.ML
changeset 2495 82ec47e0a8d3
parent 2193 b7e59795c75b
child 2753 bcde71e5f371