[isabelle] using Isabelle programmatically


I am interested in using Isabelle to simplify a formula based on a
specific theory.

If I would use the Isabelle/jEdit interface I would create a dummy theory

theory MySimp imports BaseTheory

lemma "expression to simplify = A"
  apply simp

At this point the result that I am interested is
the left hand-side of the current goal.

How can this be done programmatically? Should I use
"isabelle_process" or "isabelle console"?

Best regards,

Viorel Preoteasa

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