src/Pure/search.ML
changeset 32971 55ba9b6648ef
parent 32940 51d450f278ce
child 33335 1e189f96c393
equal deleted inserted replaced
32970:fbd2bb2489a8 32971:55ba9b6648ef