src/Pure/Syntax/parser.ML
changeset 37180 d47fe9260c24
parent 33317 b4534348b8fd
child 37216 3165bc303f66
equal deleted inserted replaced
37179:446cf1f997d1 37180:d47fe9260c24