[isabelle-dev] Creating Theorems in ML

Makarius makarius at sketis.net
Thu Feb 28 11:55:20 CET 2019

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 including any assumptions we defined in ML. 

Isabelle/ML belongs to the normal Isabelle user space, so isabelle-users
is the place to go.


More information about the isabelle-dev mailing list