src/Pure/locale.ML
changeset 8039 a901bafe4578
parent 7628 8e177a4c86a5
child 8459 c32b64394963