src/Pure/search.ML
changeset 3365 86c0d1988622
parent 2869 acee08856cc9
child 3538 ed9de44032e0