src/Pure/term_subst.ML
changeset 70820 77c8b8e73f88
parent 69023 cef000855cf4
child 74200 17090e27aae9
equal deleted inserted replaced
70819:ed89f20de7ab 70820:77c8b8e73f88