src/Pure/search.ML
changeset 14693 4deda204e1d8
parent 14160 6750ff1dfc32
child 15531 08c8dad8e399
equal deleted inserted replaced
14692:b8d6c395c9e2 14693:4deda204e1d8