src/Pure/General/scan.ML
changeset 62387 ad3eb2889f9a
parent 61476 1884c40f1539
child 62491 7187cb7a77c5