src/Pure/Isar/locale.ML
changeset 22421 51a18dd1ea86
parent 22351 587845efb4cf
child 22523 19e4fd6ffcaa