src/Pure/Syntax/lexicon.ML
changeset 60473 7dc683911e5d
parent 59196 73a6403637b3
child 61476 1884c40f1539
equal deleted inserted replaced
60472:f60f6f9baf64 60473:7dc683911e5d