src/Pure/Syntax/syntax.ML
changeset 62902 3c0f53eae166
parent 62897 8093203f0b89
child 63345 70b2313f9c52