src/Pure/General/scan.ML
changeset 17740 fc385ce6187d
parent 16803 014090d1e64b
child 18683 a8f9c192f6d1
equal deleted inserted replaced
17739:eddebb044a62 17740:fc385ce6187d