Email Gateway (Jul 21 2026 at 11:29): Email Gateway (Jul 21 2026 at 11:29):From: Lawrence Paulson <lp15@cam.ac.uk>
I’ve been trying to figure out a looping sublocale declaration of the form
sublocale id: locale_name args
but, according to our documentation (Tutorial to Locales and Locale Interpretation), this syntax (the colon) is not even legal. What does this declaration mean?
Larry
Email Gateway (Jul 21 2026 at 11:42):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Instantiate "locale_name args" as a sublocale of the current locale, and
prefix all names that come from this instantiation with "id"
the documentation in isar-ref allows sublocale <locale_expr>, and
locale_expr can have an instance with a qualifier.
--
Peter
On 21/07/2026 10:50, Lawrence Paulson wrote:
I’ve been trying to figure out a looping sublocale declaration of the form
sublocale id: locale_name args
but, according to our documentation (Tutorial to Locales and Locale Interpretation), this syntax (the colon) is not even legal. What does this declaration mean?
Larry
Last updated: Jul 22 2026 at 14:00 UTC