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 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