src/Pure/Syntax/syntax.ML
changeset 21910 5b553ed23251
parent 21826 b90d927e0a4b
child 21962 279b129498b6