src/Pure/Isar/outer_parse.ML
changeset 28337 93964076e7b8
parent 28302 ef86de9c98aa
child 28941 128459bd72d2
equal deleted inserted replaced
28336:a8edf4c69a79 28337:93964076e7b8