src/Pure/General/scan.ML
changeset 68170 7e1daf6f2578
parent 62491 7187cb7a77c5
child 78817 30bcf149054d
equal deleted inserted replaced
68169:395432e7516e 68170:7e1daf6f2578