src/Pure/Syntax/syntax.ML
changeset 70187 2082287357e6
parent 69971 4e98239aa083
child 70443 a21a96eda033