src/HOL/Lex/Scanner.ML
changeset 11295 66925f23ac7f
parent 5323 028e00595280