src/Pure/Syntax/lexicon.ML
changeset 43851 f7f8cf0a1536
parent 43432 224006e5ac46
child 43947 9b00f09f7721
equal deleted inserted replaced
43850:7f2cbc713344 43851:f7f8cf0a1536