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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
