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.

Larry

> On 23 May 2019, at 16:54, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> 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.