src/HOL/Subst/Unify.ML
changeset 5789 7d4ac02677a6
parent 5278 a903b66822e2
child 8624 69619f870939