src/Pure/Syntax/lexicon.ML
changeset 1868 836950047d85
parent 1507 f600215b6ea7
child 2363 963285471dc5