src/Pure/Syntax/parser.ML
changeset 33145 1a22f7ca1dfc
parent 32738 15bb09ca0378
child 33037 b22e44496dc2