src/HOL/Import/scan.ML
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2006-02-17 obua 2006-02-17 use monomorphic sequences / scanners
2006-02-16 obua 2006-02-16 improved scanning