src/Pure/Syntax/lexicon.ML
changeset 69014 a2c042364efc
parent 67556 5f86e2a9c59c
child 69042 6e9df530b441