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