src/Pure/Syntax/syntax.ML
changeset 35311 8f9a66fc9f80
parent 35263 9927471cca35
child 35394 11f58c600707