src/Pure/search.ML
changeset 12135 e370e5d469c2
parent 9411 0d5a171db2f0
child 12262 11ff5f47df6e
equal deleted inserted replaced
12134:7049eead7a50 12135:e370e5d469c2