src/Pure/Isar/local_syntax.ML
changeset 33126 bb8806eb5da7
parent 32738 15bb09ca0378
child 33387 acea2f336721