src/Pure/Syntax/syntax.ML
changeset 63201 f151704c08e4
parent 62897 8093203f0b89
child 63345 70b2313f9c52