src/Pure/locale.ML
changeset 7638 f586d7995474
parent 7628 8e177a4c86a5
child 8459 c32b64394963