src/Pure/search.ML
changeset 35144 8b8302da3a55
parent 33380 cd6023a9a922
child 35408 b48ab741683b