src/Pure/Isar/locale.ML
changeset 58797 6d71f19a9fd6
parent 58028 e4250d370657
child 59296 002d817b4c37