[isabelle] using Isabelle programmatically



Hello,

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
begin

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.