src/Pure/Syntax/lexicon.ML
changeset 36952 338c3f8229e4
parent 35428 bd7d6f65976e
child 38237 8b0383334031
equal deleted inserted replaced
36951:985c197f2fe9 36952:338c3f8229e4