src/HOL/Lex/Prefix.ML
changeset 5526 e7617b57a3e6
parent 5456 d2ab1264afd4
child 5609 03d74c85a818