src/Pure/Isar/outer_syntax.ML
changeset 33930 6a973bd43949
parent 33223 d27956b4d3b4
child 36950 75b8f26f2f07
equal deleted inserted replaced
33929:e7685297e9da 33930:6a973bd43949