| changeset 36714 | ae84ddf03c58 |
| parent 36645 | 30bd207ec222 |
| child 36808 | cbeb3484fa07 |
--- a/NEWS Thu May 06 17:55:12 2010 +0200 +++ b/NEWS Thu May 06 17:59:19 2010 +0200 @@ -140,6 +140,8 @@ *** HOL *** +* Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. + * Theory 'Finite_Set': various folding_* locales facilitate the application of the various fold combinators on finite sets.