src/HOL/Subst/Unify.ML
changeset 9448 755330e55e18
parent 9371 2f06293f291a
child 9736 332fab43628f
equal deleted inserted replaced
9447:e5180c869772 9448:755330e55e18