src/Pure/Isar/local_syntax.ML
changeset 33930 6a973bd43949
parent 33387 acea2f336721
child 35412 b8dead547d9e