| changeset 36726 | 47ba1770da8e |
| parent 36714 | ae84ddf03c58 |
| child 36808 | cbeb3484fa07 |
--- a/NEWS Thu May 06 11:08:19 2010 -0700 +++ b/NEWS Fri May 07 09:59:59 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.