src/Pure/search.ML
changeset 29605 f2924219125e
parent 29269 5c25a2012975
child 32738 15bb09ca0378