src/Pure/Syntax/lexicon.ML
changeset 12249 dd9a51255855
parent 11697 8dd899efbd35
child 12785 27debaf2112d
equal deleted inserted replaced
12248:f059876ef1d3 12249:dd9a51255855