src/Pure/Isar/locale.ML
changeset 30190 479806475f3c
parent 29576 669b560fc2b9
child 30223 24d975352879