changeset 20169 | 52173f7687fd |
parent 20136 | 8e92a8f9720b |
child 20188 | 8b22026445af |
--- a/NEWS Wed Jul 19 19:25:58 2006 +0200 +++ b/NEWS Wed Jul 19 23:22:22 2006 +0200 @@ -497,6 +497,11 @@ * Support for hex (0x20) and binary (0b1001) numerals. +*** HOL-Algebra *** + +* Method algebra is now set up via an attribute. For examples see CRing.thy. + INCOMPATIBILITY: the method is now weaker on combinations of algebraic structures. + *** HOL-Complex *** * Theory Real: new method ferrack implements quantifier elimination