src/HOL/Lex/Prefix.ML
changeset 3362 0b268cff9344
parent 2130 53b6e0bc8ccf
child 3842 b55686a7b22c