src/Pure/locale.ML
changeset 5253 82a5ca6290aa
parent 5244 5313f781efe0
child 5729 5d66410cceae