[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 next step we would like to create a theorem from ML,  e.g.

locale MyLocale =
  fixes S::"nat set"

lemma foo:
  "A ==> (A ==> B) ==> B"


We tried using Local_Theory.note with the Goal or Thm structures, but apart 
from trivial True ==> True there is not much success. Moreover, the example 
(3.7 Theorems) in the cookbook doesn't seem to work with 'Illegal fixed 
variable: "P"'

I'm thankful for any pointers to examples or descriptions on how to add/define 
a lemma/theorem inside a locale from an ML file.

-- Reto
isabelle-dev mailing list

Reply via email to