src/Pure/Syntax/syntax.ML
changeset 4030 ca44afcc259c
parent 3830 7797327eca1d
child 4101 e8ad51c88be9
equal deleted inserted replaced
4029:22f2d1b17f97 4030:ca44afcc259c