src/Pure/search.ML
changeset 4271 3a82492e70c5
parent 4270 957c887b89b5
child 5693 998af7667fa3