src/Pure/old_term.ML
changeset 31483 88210717bfc8
parent 30364 577edc39b501
child 35408 b48ab741683b
equal deleted inserted replaced
31482:7288382fd549 31483:88210717bfc8