src/Pure/Syntax/lexicon.ML
changeset 12197 d9320fb0a570
parent 11697 8dd899efbd35
child 12785 27debaf2112d