equal
deleted
inserted
replaced
708 * Formalisation of ideals and the quotient construction over rings. |
708 * Formalisation of ideals and the quotient construction over rings. |
709 |
709 |
710 * Order and lattice theory no longer based on records. |
710 * Order and lattice theory no longer based on records. |
711 INCOMPATIBILITY. |
711 INCOMPATIBILITY. |
712 |
712 |
|
713 * Renamed lemmas least_carrier -> least_closed and |
|
714 greatest_carrier -> greatest_closed. INCOMPATIBILITY. |
|
715 |
713 * Method algebra is now set up via an attribute. For examples see |
716 * Method algebra is now set up via an attribute. For examples see |
714 CRing.thy. INCOMPATIBILITY: the method is now weaker on combinations |
717 Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations |
715 of algebraic structures. |
718 of algebraic structures. |
716 |
719 |
717 * Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. |
720 * Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. |
718 |
721 |
719 |
722 |