src/Pure/Syntax/lexicon.ML
changeset 43576 ebeda6275027
parent 43432 224006e5ac46
child 43947 9b00f09f7721
equal deleted inserted replaced
43575:cfb2077cb2db 43576:ebeda6275027