Hi John, There is Locale.init, which seems to be what you want.
Clemens Quoting John Munroe <[email protected]>:
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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
