Re: [isabelle] accessing ML definitions in isabelle_process

On Tue, 28 Apr 2015, Viorel Preoteasa wrote:

Using Isabelle/ML snippets inside a proper theory context seems oriented towards a user interface. But I need to do this in batch mode. If I use this approach I have to create always a theory file, and then load it using use_thy. I would need to do this for every small call that I need.

I was talking about batch mode already. You could e.g. put all your tool setup in a static .thy (or .thy that loads a .ML via ML_file). It could refer to some environment variables to get dynamic input from somewhere else, e.g. another tmp file.

There are many more possibilities, e.g. using Isabelle/Scala for the systems programming.

fun simplifya s ct th =

The "ct" here seems to be a Proof.context, and the one and only one naming convention is "ctxt". See also the "implementation" manual.

I can define this code in a ml file, except:

val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
val Set_all_bool_eq = @{thm Set.all_bool_eq};

probably there is a way to get these theorems at the toplevel of isabelle_process
using the context and the theory.

Isabelle/ML files always refer to a proper theory context. So we are back to the start.


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