src/HOL/Lex/Scanner.ML
changeset 6443 6d5d3ecedf50
parent 5323 028e00595280
equal deleted inserted replaced
6442:6a95ceaa977e 6443:6d5d3ecedf50