src/Pure/Syntax/parser.ML
changeset 19423 51eeee99bd8f
parent 19305 5c16895d548b
child 19482 9f11af8f7ef9