src/Pure/Syntax/lexicon.ML
changeset 42550 3031d342d514
parent 42476 d0bc1268ef09
child 43432 224006e5ac46