Re: [isabelle] Conflicting rules in default simps vs. algebraic rule collections.

The problem is that divide_simps already exists, with the objective of eliminating all occurrences of the division sign in expressions. It is a good deal more effective than field_simps in many situations.

Larry Paulson

> On 2 Mar 2019, at 10:29, Florian Haftmann <florian.haftmann at> wrote:
> * »divide_simps« would be a quite fitting name, quoth Field.thy: ‹Lemmas
> ‹divide_simps› move division to the outside and eliminates them on
> (in)equalities.›
> I am currently inclined to pursue the latter option, which would also
> suggest to generalize the relevant lemmas to a common ancestor type class.

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