src/Pure/Syntax/syntax.ML
changeset 12328 7c4ec77a8715
parent 12316 79138d75405f
child 12785 27debaf2112d