src/Pure/Isar/outer_syntax.ML
changeset 29252 ea97aa6aeba2
parent 28436 4faf705a177d
child 29311 4c830711e6f1
equal deleted inserted replaced
29251:8f84a608883d 29252:ea97aa6aeba2