src/Pure/Isar/local_syntax.ML
changeset 38664 7215ae18f44b
parent 35429 afa8cf9e63d8
equal deleted inserted replaced
38654:0b1a63d06805 38664:7215ae18f44b