5273 fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY. |
5273 fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY. |
5274 |
5274 |
5275 * HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY. |
5275 * HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY. |
5276 |
5276 |
5277 * HOL-Word: New extensive library and type for generic, fixed size |
5277 * HOL-Word: New extensive library and type for generic, fixed size |
5278 machine words, with arithemtic, bit-wise, shifting and rotating |
5278 machine words, with arithmetic, bit-wise, shifting and rotating |
5279 operations, reflection into int, nat, and bool lists, automation for |
5279 operations, reflection into int, nat, and bool lists, automation for |
5280 linear arithmetic (by automatic reflection into nat or int), including |
5280 linear arithmetic (by automatic reflection into nat or int), including |
5281 lemmas on overflow and monotonicity. Instantiated to all appropriate |
5281 lemmas on overflow and monotonicity. Instantiated to all appropriate |
5282 arithmetic type classes, supporting automatic simplification of |
5282 arithmetic type classes, supporting automatic simplification of |
5283 numerals on all operations. |
5283 numerals on all operations. |