src/Pure/locale.ML
changeset 10168 50be659d4222
parent 8908 25f2bdc02123
child 10349 78434c9a54fd