src/Pure/locale.ML
changeset 9413 ba209591a8d4
parent 8908 25f2bdc02123
child 10349 78434c9a54fd