Re: [isabelle] accessing ML definitions in isabelle_process



On Tue, 28 Apr 2015, Viorel Preoteasa wrote:

I have a theory which defines

theory TestML imports Main
begin
ML
{*
   val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
   val Set_all_bool_eq = @{thm Set.all_bool_eq};
*}
end

How can I access these objects from the isabelle_process?

I know that I can load the theory file using use_thy "TestML",
but I could not figure out how to access these names.

Almost everything in Isabelle lives within a formal theory context, including the ML environment. It is merely a historical accident of the Isabelle/Pure bootstrap process that the ML content of Pure.thy is also dumped onto the naked ML toplevel of isabelle_process or isabelle console.

So the canonical approach is to evaluate Isabelle/ML snippets inside a proper theory context like Main above. The remaining question is how to achieve that for your application. E.g. one could produce a temporary
.thy file on the spot and load that with use_thy.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.