1.1 --- a/NEWS Tue May 11 11:58:34 2010 -0700
1.2 +++ b/NEWS Tue May 11 12:05:19 2010 -0700
1.3 @@ -143,7 +143,11 @@
1.4 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
1.5 no longer shadowed. INCOMPATIBILITY.
1.6
1.7 -* Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY.
1.8 +* Dropped theorem duplicate comp_arith; use semiring_norm instead.
1.9 +INCOMPATIBILITY.
1.10 +
1.11 +* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
1.12 +INCOMPATIBILITY.
1.13
1.14 * Theory 'Finite_Set': various folding_* locales facilitate the application
1.15 of the various fold combinators on finite sets.