src/Pure/locale.ML
changeset 5863 9935800edf58
parent 5782 7559f116cb10
child 6022 259e4f2114e1