src/Pure/Syntax/parser.ML
changeset 42581 398fff2c6b8f
parent 42374 b9a6b465da25
child 44102 954e9d6782ea
equal deleted inserted replaced
42580:04cae06f0b99 42581:398fff2c6b8f