[isabelle] scala interface



Hi,

I am trying to use the scala library Pure.jar to communicate with the Isabelle process. A typical use case is to send a theory snipped like the following and to check whether the proof attempt succeeds:

theory Test imports Main begin

lemma foo:
fixes x :: bool
assumes "x = True"
shows "x | x"
using assms
by simp

I have already discovered the Isabelle_System.init method and I am aware of the classes "Isabelle_Process" and "Session". My attempts to communicate the above snippet to an Isabelle_Process failed due to my unawareness of the input format of Isabelle_Process.input. (Perhaps, this is not the intended interface anyway?) I also tried to use Session.init_node, but I am not sure how to choose the parameters and how to receive the result.

I would appreciate any help on this very much!

Best,
Matthias





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