src/Pure/term_subst.ML
changeset 37321 9d7cfae95b30
parent 36766 33e4246edf29
child 43326 47cf4bc789aa
equal deleted inserted replaced
37320:06c7a2f231fe 37321:9d7cfae95b30