src/Pure/Isar/outer_syntax.ML
changeset 75087 f3fcc7c5a0db
parent 74964 77a96ed74340
child 76815 974f2c104f63
equal deleted inserted replaced
75086:4cc719621825 75087:f3fcc7c5a0db