src/HOL/Lex/Prefix.ML
changeset 2003 b48f066d52dc
parent 1894 c2c8279d40f0
child 2130 53b6e0bc8ccf