| changeset 36808 | cbeb3484fa07 |
| parent 36714 | ae84ddf03c58 |
| child 36811 | 4ab4aa5bee1c |
--- a/NEWS Mon May 10 15:33:32 2010 +0200 +++ b/NEWS Tue May 11 08:29:42 2010 +0200 @@ -140,6 +140,9 @@ *** HOL *** +* Theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct; +theorem Int.int_induct is no longer shadowed. INCOMPATIBILITY. + * Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. * Theory 'Finite_Set': various folding_* locales facilitate the application