4774 fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY. |
4774 fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY. |
4775 |
4775 |
4776 * HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY. |
4776 * HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY. |
4777 |
4777 |
4778 * HOL-Word: New extensive library and type for generic, fixed size |
4778 * HOL-Word: New extensive library and type for generic, fixed size |
4779 machine words, with arithemtic, bit-wise, shifting and rotating |
4779 machine words, with arithmetic, bit-wise, shifting and rotating |
4780 operations, reflection into int, nat, and bool lists, automation for |
4780 operations, reflection into int, nat, and bool lists, automation for |
4781 linear arithmetic (by automatic reflection into nat or int), including |
4781 linear arithmetic (by automatic reflection into nat or int), including |
4782 lemmas on overflow and monotonicity. Instantiated to all appropriate |
4782 lemmas on overflow and monotonicity. Instantiated to all appropriate |
4783 arithmetic type classes, supporting automatic simplification of |
4783 arithmetic type classes, supporting automatic simplification of |
4784 numerals on all operations. |
4784 numerals on all operations. |