src/Pure/Syntax/lexicon.ML
changeset 68446 92ddca1edc43
parent 67556 5f86e2a9c59c
child 69042 6e9df530b441