src/Pure/search.ML
changeset 5526 e7617b57a3e6
parent 4270 957c887b89b5
child 5693 998af7667fa3