src/Pure/search.ML
changeset 2003 b48f066d52dc
parent 1588 fff3738830f5
child 2143 093bbe6d333b