NEWS
changeset 46732 ac701d7f7c3b
parent 46641 8801a24f9e9a
child 46752 e9e7209eb375
equal deleted inserted replaced
46727:0162a0d284ac 46732:ac701d7f7c3b
  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.