Re: [isabelle] using Isabelle programmatically



> I need to perform this operation from within a Python program.
> I use Python to produce some terms based on some specification,
> and I need them simplified using Isabelle. The terms are using
> definitions from the supporting theory.

If you are free to choose the language of your tool, may I suggest to
consider Java or Scala: For the JVM, there is the possibility to
communicate with the prover in a canonical way (i.e.
starting/stopping/sending messages to the prover can be done with
regular function calls, instead of performing low-level process
operations and I/O).




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