equal
deleted
inserted
replaced
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 |