equal
deleted
inserted
replaced
608 is available in HOL/ex/ReflectionEx.thy |
608 is available in HOL/ex/ReflectionEx.thy |
609 |
609 |
610 |
610 |
611 *** HOL-Algebra *** |
611 *** HOL-Algebra *** |
612 |
612 |
|
613 * Formalisation of ideals and the quotient construction over rings, contributed |
|
614 by Stephan Hohe. |
|
615 |
|
616 * Order and lattice theory no longer based on records. INCOMPATIBILITY. |
|
617 |
613 * Method algebra is now set up via an attribute. For examples see CRing.thy. |
618 * Method algebra is now set up via an attribute. For examples see CRing.thy. |
614 INCOMPATIBILITY: the method is now weaker on combinations of algebraic |
619 INCOMPATIBILITY: the method is now weaker on combinations of algebraic |
615 structures. |
620 structures. |
616 |
|
617 * Formalisation of ideals and the quotient construction over rings, contributed |
|
618 by Stephan Hohe. |
|
619 |
621 |
620 * Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. |
622 * Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. |
621 |
623 |
622 |
624 |
623 *** HOL-Complex *** |
625 *** HOL-Complex *** |