src/Pure/Syntax/parser.ML
changeset 20902 a0034e545c13
parent 20854 f9cf9e62d11c
child 20951 868120282837