src/Pure/term_subst.ML
changeset 78373 2deecde7f1f6
parent 74578 9bfbb5f7ec99
child 79129 2933e71f4e09
equal deleted inserted replaced
78372:30d3faa6c245 78373:2deecde7f1f6