src/Pure/Syntax/syntax.ML
changeset 35311 8f9a66fc9f80
parent 35263 9927471cca35
child 35394 11f58c600707
equal deleted inserted replaced
35309:997aa3a3e4bb 35311:8f9a66fc9f80