src/Pure/Syntax/parser.ML
changeset 43655 5742b288bb86
parent 42374 b9a6b465da25
child 44102 954e9d6782ea