src/Pure/search.ML
changeset 11916 82139d3dcdd7
parent 9411 0d5a171db2f0
child 12262 11ff5f47df6e
equal deleted inserted replaced
11915:df030220a2a8 11916:82139d3dcdd7