src/Pure/search.ML
changeset 30902 5c8618f95d24
parent 29269 5c25a2012975
child 32738 15bb09ca0378