src/Pure/search.ML
changeset 33930 6a973bd43949
parent 33380 cd6023a9a922
child 35408 b48ab741683b