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



>> * »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.

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

Just to be more explicit: I suggest exactly to re-use the *exisiting*
divide_simps, because the rules in question are both structurally and by
purpose quite similar to those already gathered there.

	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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