src/Pure/General/scan.ML
changeset 56407 8e7ebc4b30f1
parent 55104 8284c0d5bf52
child 58850 1bb0ad7827b4