src/Pure/Syntax/syntax.ML
changeset 5975 cd19eaa90f45
parent 5702 77ad51744aee
child 6167 2f354020efc3