summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |