src/Pure/Syntax/syntax.ML
changeset 4030 ca44afcc259c
parent 3830 7797327eca1d
child 4101 e8ad51c88be9