src/Pure/Isar/local_syntax.ML
changeset 20083 717b1eb434f1
parent 19660 e3ec6839c631
child 20785 d60f81c56fd4