src/HOL/Lex/MaxPrefix.ML
changeset 12913 5ac498bffb6b
parent 10338 291ce4c4b50e
equal deleted inserted replaced
12912:0e144958cf27 12913:5ac498bffb6b