src/Pure/Isar/local_syntax.ML
changeset 19826 4499a73efb1c
parent 19660 e3ec6839c631
child 20785 d60f81c56fd4