src/Pure/Isar/locale.ML
changeset 58797 6d71f19a9fd6
parent 58028 e4250d370657
child 59296 002d817b4c37
equal deleted inserted replaced
58796:cc5a9a54d340 58797:6d71f19a9fd6