src/HOL/Import/scan.ML
changeset 40749 cb6698d2dbaf
parent 40627 becf5d5187cc
equal deleted inserted replaced
40748:591b6778d076 40749:cb6698d2dbaf