[isabelle-dev] Default simprules for division in fields

[Lawrence Paulson]

A very good idea, which reduces the impact of the change on existing proofs. I am trying it out now.

Seeing no objections, I am quite likely to push this change later today.

Larry

On 4 Apr 2014, at 15:08, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> 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
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev