src/Pure/Syntax/lexicon.ML
changeset 28620 9846d772b306
parent 28413 ee73353fb87c
child 28904 3ef9489eeef5