src/Pure/consts.ML
changeset 80571 673add17a05e
parent 79471 593fdddc6d98
child 81220 3d09d6f4c5b1
equal deleted inserted replaced
80570:4d4f107a778f 80571:673add17a05e