src/HOL/Lex/Prefix.ML
changeset 2250 891eb76b8045
parent 2130 53b6e0bc8ccf
child 3842 b55686a7b22c