src/Pure/Syntax/syntax.ML
changeset 12412 d0857ea70f23
parent 12316 79138d75405f
child 12785 27debaf2112d