src/Pure/Isar/outer_syntax.ML
changeset 7145 c05373eebee3
parent 7104 247e4247b64e
child 7192 30a67acd0d7e
equal deleted inserted replaced
7144:0feee8201d67 7145:c05373eebee3