src/Pure/Isar/locale.ML
changeset 37380 35815ce9218a
parent 37133 1d048c6940c8
child 37471 907e13072675