src/Pure/search.ML
changeset 1868 836950047d85
parent 1588 fff3738830f5
child 2143 093bbe6d333b