src/Pure/variable.ML
changeset 70009 435fb018e8ee
parent 69576 cfac69e7b962
child 70304 1514efa1e57a