src/HOL/Lex/Prefix.ML
changeset 2531 7cfa1a9c744d
parent 2130 53b6e0bc8ccf
child 3842 b55686a7b22c