src/Pure/Syntax/syntax.ML
changeset 5975 cd19eaa90f45
parent 5702 77ad51744aee
child 6167 2f354020efc3
equal deleted inserted replaced
5974:6acf3ff0f486 5975:cd19eaa90f45