src/Pure/Syntax/syntax.ML
changeset 41903 39fd77f0ae59
parent 41711 3422ae5aff3a
child 42043 2055515c9d3f
equal deleted inserted replaced
41902:1941b3315952 41903:39fd77f0ae59