[isabelle-dev] Context of a locale?

[Clemens Ballarin]

Hi John,

There is Locale.init, which seems to be what you want.

Clemens

Quoting John Munroe <munddr at gmail.com>:

> Hello
>
> Does anyone know of a way to obtain the context of a given locale
> name? There doesn't seem to be an appropriate function for this in
> locale.ML.
>
> Any help will be appreciated. Thanks.
>
> Regards
> - John
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>