src/Pure/Syntax/parser.ML
changeset 80098 c06c95576ea9
parent 79079 01f9128ec655
child 80927 81b942537dd1
equal deleted inserted replaced
80096:83fa23ca40e5 80098:c06c95576ea9