src/Pure/Syntax/lexicon.ML
changeset 23615 40ab945ef5ff
parent 22686 68496cc300a4
child 23784 75e6b9dd5336