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.
> On 2 Mar 2019, at 10:29, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> * »divide_simps« would be a quite fitting name, quoth Field.thy: ‹Lemmas
> ‹divide_simps› move division to the outside and eliminates them on
> 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