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.
I don't think it is a good policy to ask for comments on a change and then say that you will push it half a day later. I for one am not convinced by the utility of the change. 1. Your changeset shows quite a number of proofs where the rules need to be added by hand but in all of HOL there is only one proof where divide_minus_left is removed. Hence the current setup seems to work not that badly. 2. I see little difference between a normal form where "/" is pulled out and one where "-" is. You may have to deal with one more case if "-" is pulled out. But can you give an example where pulling "/" out is a big win over "-"? Tobias > Larry > > On 4 Apr 2014, at 15:08, Florian Haftmann > <florian.haftm...@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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev