src/Pure/Syntax/lexicon.ML
changeset 21175 98c0405f5493
parent 20664 ffbc5a57191a
child 21774 3f9324ff06e3