src/Pure/Syntax/syntax.ML
changeset 62944 3ee643c5ed00
parent 62897 8093203f0b89
child 63345 70b2313f9c52