On 04/04/2014 18:10, Florian Haftmann wrote: >> Florian, can you give an example where previously field_simps was too >> weak but with the two additional rules it works? > > Well, your example seems to indicate that even field_simps is too strong as > declaration.
Which example? I didn't give one... Tobias > Florian > >> >> Tobias >> >> On 04/04/2014 17:37, Lawrence Paulson wrote: >>> 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 >>> <[email protected]> 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 [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 >>> >> >>> _______________________________________________ >> 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
