src/Pure/search.ML
changeset 4687 8cec457a8961
parent 4270 957c887b89b5
child 5693 998af7667fa3