src/Pure/Syntax/lexicon.ML
changeset 17120 4ddeef83bd66
parent 16150 c33fe18456fa
child 18189 b44d53088108
equal deleted inserted replaced
17119:b241ba3eb4db 17120:4ddeef83bd66