src/Pure/Syntax/syntax.ML
changeset 194 06e31ac55dd1
parent 175 c02750f7f604
child 237 a7d3e712767a
equal deleted inserted replaced
193:b2be328e00c3 194:06e31ac55dd1