src/HOL/Lex/MaxPrefix.ML
changeset 13012 f8bfc61ee1b5
parent 10338 291ce4c4b50e