[isabelle-dev] HOL/Rings.thy: {left,right}_distrib

[Tjark Weber]

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