src/Pure/Syntax/lexicon.ML
changeset 81552 4717d3bf5752
parent 81225 2157039256d3
child 81596 af21a61dadad