src/HOL/Subst/Unifier.ML
changeset 14502 0c135fa75626
parent 5278 a903b66822e2