src/Pure/General/scan.ML
changeset 24547 64c20ee76bc1
parent 24025 77e3e5781a99
child 24595 5c290506fbc0