[isabelle-dev] Default simprules for division in fields
nipkow at in.tum.de
Fri Apr 4 18:26:29 CEST 2014
Florian, I was confused and you may well be right: if those two rules are no
longer simp rules, it looks like field_simps no longer does its job properly.
Most likely they should be added there as you suggested.
On 04/04/2014 16:08, Florian Haftmann wrote:
>> lemma divide_minus_left [simp]: "(-a) / b = - (a / b)" lemma
>> divide_minus_right [simp]: "a / - b = - (a / b)”
>> It would be a mistake to reorient the simprules, but I am suggesting that
>> they should not be declared as simprules with either orientation.
>> lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)" lemma
>> divide_minus_right [field_simps]: "a / - b = - (a / b)”
> _______________________________________________ isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev