Re: [isabelle] Algebraic rule collections

The purpose of divide_simps is to eliminate division from arithmetic expressions in equations and inequalities. I introduced it in order to simplify the results of differentiation but it seems to have many other applications.


> On 23 May 2019, at 16:54, Florian Haftmann <florian.haftmann at> wrote:
> The specific property of sign_simps and divide_simps is that goals
> may be split.  

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