src/Pure/General/scan.ML
changeset 57896 2d037f8dc4d5
parent 55104 8284c0d5bf52
child 58850 1bb0ad7827b4