src/Pure/Syntax/syntax.ML
changeset 69014 a2c042364efc
parent 69003 a015f1d3ba0c
child 69071 3ef82592dc22
equal deleted inserted replaced
69013:bb4e4c253ebe 69014:a2c042364efc