src/Pure/search.ML
changeset 5548 5cd3396802f5
parent 4270 957c887b89b5
child 5693 998af7667fa3