src/Pure/term_subst.ML
changeset 43149 9675d631df3d
parent 36766 33e4246edf29
child 43326 47cf4bc789aa
equal deleted inserted replaced
43148:092e38108f3f 43149:9675d631df3d