src/Pure/General/scan.ML
changeset 23780 a0e7305dd0cb
parent 23699 5a4527f3ac79
child 24025 77e3e5781a99