On Tue, 2012-10-16 at 17:43 +0200, Tobias Nipkow wrote: > Am 16/10/2012 13:22, schrieb Tjark Weber: > > Class semiring in HOL/Rings.thy [1] assumes > > > > left_distrib: "(a + b) * c = a * c + b * c" > > right_distrib: "a * (b + c) = a * b + a * c"
> We should certainly not contradict the mathematical usage. I favour Jasmin's > proposal because distributivity is such a well-known notion that I would not > like to get rid of it. [...] See now Isabelle/a8cc904a6820 and AFP/b162ed761092. Please let me know if anything breaks; these theorem names were used all over the place. There are other occurrences of left/right distributivity theorems (e.g., for setsum), both in theories and in ML sources. I haven't touched those, so at least some of them probably still follow the above unconventional naming scheme. Best regards, Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
