equal
deleted
inserted
replaced
142 |
142 |
143 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is |
143 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is |
144 no longer shadowed. INCOMPATIBILITY. |
144 no longer shadowed. INCOMPATIBILITY. |
145 |
145 |
146 * Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. |
146 * Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. |
|
147 |
|
148 * Dropped normalizing. Use semiring classes directly. INCOMPATIBILITY. |
147 |
149 |
148 * Theory 'Finite_Set': various folding_* locales facilitate the application |
150 * Theory 'Finite_Set': various folding_* locales facilitate the application |
149 of the various fold combinators on finite sets. |
151 of the various fold combinators on finite sets. |
150 |
152 |
151 * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT' |
153 * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT' |