src/Pure/search.ML
changeset 23597 ab67175ca8a5
parent 23178 07ba6b58b3d2
child 23841 598839baafed
equal deleted inserted replaced
23596:f8381a95c49c 23597:ab67175ca8a5