src/Pure/variable.ML
changeset 70753 c5232e6fb10b
parent 70733 ce1afe0f3071
child 70843 cc987440d776
equal deleted inserted replaced
70750:07673e7cb5e6 70753:c5232e6fb10b