src/Pure/locale.ML
changeset 9619 6125cc9efc18
parent 8908 25f2bdc02123
child 10349 78434c9a54fd