src/Pure/General/scan.ML
changeset 40525 14a2e686bdac
parent 38875 c7a66b584147
child 40627 becf5d5187cc
equal deleted inserted replaced
40524:6131d7a78ad3 40525:14a2e686bdac