src/Pure/Syntax/syntax.ML
changeset 70076 3b3089863eda
parent 69971 4e98239aa083
child 70443 a21a96eda033