src/Pure/Isar/local_syntax.ML
changeset 37978 548f3f165d05
parent 35429 afa8cf9e63d8
equal deleted inserted replaced
37977:3ceccd415145 37978:548f3f165d05