src/Pure/search.ML
changeset 80266 d52be75ae60b
parent 62919 9eb0359d6a77
equal deleted inserted replaced
80265:cb795bbce540 80266:d52be75ae60b