src/HOL/Import/scan.ML
changeset 42150 b0c0638c4aad
parent 40627 becf5d5187cc
equal deleted inserted replaced
42149:7e6f4ca198bb 42150:b0c0638c4aad