src/Pure/search.ML
changeset 34173 458ced35abb8
parent 33380 cd6023a9a922
child 35408 b48ab741683b