src/Pure/Syntax/lexicon.ML
changeset 67945 984c3dc46cc0
parent 67556 5f86e2a9c59c
child 69042 6e9df530b441