src/Pure/search.ML
changeset 2923 f675fb52727b
parent 2869 acee08856cc9
child 3538 ed9de44032e0