src/Pure/Syntax/lexicon.ML
changeset 63905 1c3dcb5fe6cb
parent 62819 d3ff367a16a0
child 64275 ac2abc987cf9