src/Pure/Syntax/syntax.ML
changeset 69014 a2c042364efc
parent 69003 a015f1d3ba0c
child 69071 3ef82592dc22