[isabelle] using Isabelle programmatically
I am interested in using Isabelle to simplify a formula based on a
If I would use the Isabelle/jEdit interface I would create a dummy theory
theory MySimp imports BaseTheory
lemma "expression to simplify = A"
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"?
This archive was generated by a fusion of
Pipermail (Mailman edition) and