Re: [isabelle] The Symbolic Newton Method


On Fri, 2009-03-20 at 13:45 +0100, Jens Doll wrote:
> I now wonder, if the resulting expression could be reduced
> by some Isabelle tactics

I'd try "apply simp", or perhaps "apply auto".  Various useful
theorems, e.g., "0 * a = 0", are installed as simplification
rules by default.  Others may have to be added manually.

If you only care about simplification, rather than theorem
proving, a computer algebra system (such as Maple) might be
the better tool for this task.


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