Re: [isabelle] a simplifier question 2



On 08.06.2015 11:42, Manuel Eberl wrote:
> Equations added to the simp set are not simplified themselves, so the
> simplifier will only rewrite "a^(3+3)", but still not "a^6". It might
> not even rewrite "a^(3+3)" to "a^3 * a^3", because "3+3" might be
> rewritten to "6" first.
That issue is shortly touched upon in Gerwin's style guide[1] in the
section " Decide on good normal forms and use them consistently."

[1] http://proofcraft.org/blog/isabelle-style-part2.html



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