src/Pure/search.ML
changeset 27184 b1483d423512
parent 23841 598839baafed
child 29269 5c25a2012975