src/Pure/search.ML
changeset 5893 c755dfd02509
parent 5754 98744e38ded1
child 5956 ab4d13e9e77a