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