src/HOL/Subst/Unifier.ML
changeset 5003 f73ad32e44d3
parent 4719 21af5c0be0c9
child 5069 3ea049f7979d