On 28/02/2019 11:49, Achermann Reto wrote:
>
> [apologies in advance if this should have gone to the isabelle-users list]
>
> We are using ML in a project where we need to create a locale in HOL
> from ML code. We managed to create the locale (local_theory) using
> Expression.add_locale_cmd
Hi,
[apologies in advance if this should have gone to the isabelle-users list]
We are using ML in a project where we need to create a locale in HOL from ML
code. We managed to create the locale (local_theory) using
Expression.add_locale_cmd including any assumptions we defined in ML.
As a
