src/Pure/search.ML
changeset 19123 a278d1e65c1d
parent 18921 f47c46d7d654
child 19482 9f11af8f7ef9