src/Pure/Isar/locale.ML
changeset 80596 166c61e21bfc
parent 80298 f3bfec3b02f0
child 80910 406a85a25189