src/Pure/General/scan.ML
changeset 33178 70522979c7be
parent 32784 1a5dde5079ac
child 33955 fff6f11b1f09