src/Pure/Syntax/syntax.ML
changeset 81197 794b10baf0de
parent 81176 c0522b2d3df6
child 81588 81a72b7fcb0c
equal deleted inserted replaced
81196:eb397024b496 81197:794b10baf0de