src/Pure/term_subst.ML
changeset 23961 9e7e1e309ebd
parent 21607 3698319f6503
child 29269 5c25a2012975
equal deleted inserted replaced
23960:c07ae96cbfc4 23961:9e7e1e309ebd