src/Pure/General/scan.ML
changeset 17740 fc385ce6187d
parent 16803 014090d1e64b
child 18683 a8f9c192f6d1