NEWS
changeset 7313 300487ddfba9
parent 7300 8439bf404c28
child 7320 e89fd7d0a624
equal deleted inserted replaced
7312:523fb2832b30 7313:300487ddfba9
   122 NB: At the moment, these decision procedures do not cope with mixed
   122 NB: At the moment, these decision procedures do not cope with mixed
   123 nat/int formulae where the two parts interact, such as `m < n ==>
   123 nat/int formulae where the two parts interact, such as `m < n ==>
   124 int(m) < int(n)'.
   124 int(m) < int(n)'.
   125 
   125 
   126 * HOL/Numeral provides a generic theory of numerals (encoded
   126 * HOL/Numeral provides a generic theory of numerals (encoded
   127 efficiently as bit strings); setup for types nat and int is in place;
   127 efficiently as bit strings); setup for types nat/int/real is in place;
   128 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
   128 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
   129 int, existing theories and proof scripts may require a few additional
   129 int, existing theories and proof scripts may require a few additional
   130 type constraints;
   130 type constraints;
   131 
   131 
   132 * integer division and remainder can now be performed on constant
   132 * integer division and remainder can now be performed on constant