src/Pure/Isar/local_syntax.ML
changeset 33930 6a973bd43949
parent 33387 acea2f336721
child 35412 b8dead547d9e
equal deleted inserted replaced
33929:e7685297e9da 33930:6a973bd43949