src/Pure/Syntax/lexicon.ML
changeset 43526 2b92a6943915
parent 43432 224006e5ac46
child 43947 9b00f09f7721
equal deleted inserted replaced
43525:8f28a91ea135 43526:2b92a6943915