src/Pure/Isar/local_syntax.ML
changeset 40417 a29b2fee592b
parent 35429 afa8cf9e63d8
equal deleted inserted replaced
40416:6461fc0f9f47 40417:a29b2fee592b