[isabelle-dev] Default simprules for division in fields

[Tobias Nipkow]

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.

Tobias


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.
> 
> Maybe
>> lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)" lemma
>> divide_minus_right [field_simps]: "a / - b = - (a / b)”
> instead?
> 
> Florian
> 
> 
> 
> _______________________________________________ isabelle-dev mailing list 
> isabelle-dev at in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>