src/Pure/Syntax/syntax.ML
changeset 4873 b5999638979e
parent 4703 a50ab39756db
child 4887 bbc13af86c16
equal deleted inserted replaced
4872:33e7cdc20681 4873:b5999638979e