Hi Tjark, Am 16.10.2012 um 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" > > This is different from the terminology used in Wikipedia [2], > MathWorld [3] and much of the literature, which call the first > property right distributive, and the second left distributive. > > The difference in terminology becomes more than just slightly > confusing when one wants to define near-semirings [4] and related > structures, which satisfy only one of the two distributive laws. > > A rose by any other name would smell as sweet. Any opinions on > swapping the names above? My only opinion is that the "swapping" should be done by inventing new names first, e.g. "distrib_left" and "distrib_right", so that porting is an idempotent operation. Whether the old names should be temporarily available for compatibility, and whether "distrib_xxx" should later be renamed "xxx_distrib", are questions where I have no ready-made answer. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
