src/Pure/Syntax/lexicon.ML
changeset 59017 80290f06a810
parent 58854 b979c781c2db
child 59196 73a6403637b3