src/Pure/term_subst.ML
changeset 42240 5a4d30cd47a7
parent 36766 33e4246edf29
child 43326 47cf4bc789aa
equal deleted inserted replaced
42239:e48baf91aeab 42240:5a4d30cd47a7