src/Pure/search.ML
changeset 23730 8866c87d1a16
parent 23178 07ba6b58b3d2
child 23841 598839baafed