summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 07 Jan 2021 13:23:54 +0100 | |

changeset 73094 | 86a18742e5b2 |

parent 73093 | dc62ecc7e59a |

child 73095 | d08cbc36a99a |

clarified NEWS;

--- a/NEWS Thu Jan 07 09:14:24 2021 +0000 +++ b/NEWS Thu Jan 07 13:23:54 2021 +0100 @@ -171,31 +171,30 @@ division, instantiated for type int. * Theory "Multiset": removed misleading notation \<Union># for sum_mset; -replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also -exists now. - -* Self-contained library theory "Word" taken over from former session -"HOL-Word". - -* Theory "Word": Type word is restricted to bit strings consisting of at -least one bit. INCOMPATIBILITY. - -* Theory "Word": Bit operations NOT, AND, OR, XOR are based on generic -algebraic bit operations from theory "HOL-Library.Bit_Operations". -INCOMPATIBILITY. - -* Theory "Word": Most operations on type word are set up for transfer -and lifting. INCOMPATIBILITY. - -* Theory "Word": Generic type conversions. INCOMPATIBILITY, sometimes -additional rewrite rules must be added to applications to get a -confluent system again. - -* Theory "Word": Uniform polymorphic "mask" operation for both types int -and word. INCOMPATIBILITY. - -* Theory "Word": Syntax for signed compare operators has been -consolidated with syntax of regular compare operators. Minor +replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also exists now. + +* New theory "HOL-Library.Word" takes over material from former session +"HOL-Word". INCOMPATIBILITY: need to adjust imports. + +* Theory "HOL-Library.Word": Type word is restricted to bit strings +consisting of at least one bit. INCOMPATIBILITY. + +* Theory "HOL-Library.Word": Bit operations NOT, AND, OR, XOR are based +on generic algebraic bit operations from theory +"HOL-Library.Bit_Operations". INCOMPATIBILITY. + +* Theory "HOL-Library.Word": Most operations on type word are set up for +transfer and lifting. INCOMPATIBILITY. + +* Theory "HOL-Library.Word": Generic type conversions. INCOMPATIBILITY, +sometimes additional rewrite rules must be added to applications to get +a confluent system again. + +* Theory "HOL-Library.Word": Uniform polymorphic "mask" operation for +both types int and word. INCOMPATIBILITY. + +* Theory "HOL-Library.Word": Syntax for signed compare operators has +been consolidated with syntax of regular compare operators. Minor INCOMPATIBILITY. * Former session "HOL-Word": Various operations dealing with bit values