169 |
169 |
170 * Library theory "Signed_Division" provides operations for signed |
170 * Library theory "Signed_Division" provides operations for signed |
171 division, instantiated for type int. |
171 division, instantiated for type int. |
172 |
172 |
173 * Theory "Multiset": removed misleading notation \<Union># for sum_mset; |
173 * Theory "Multiset": removed misleading notation \<Union># for sum_mset; |
174 replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also |
174 replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also exists now. |
175 exists now. |
175 |
176 |
176 * New theory "HOL-Library.Word" takes over material from former session |
177 * Self-contained library theory "Word" taken over from former session |
177 "HOL-Word". INCOMPATIBILITY: need to adjust imports. |
178 "HOL-Word". |
178 |
179 |
179 * Theory "HOL-Library.Word": Type word is restricted to bit strings |
180 * Theory "Word": Type word is restricted to bit strings consisting of at |
180 consisting of at least one bit. INCOMPATIBILITY. |
181 least one bit. INCOMPATIBILITY. |
181 |
182 |
182 * Theory "HOL-Library.Word": Bit operations NOT, AND, OR, XOR are based |
183 * Theory "Word": Bit operations NOT, AND, OR, XOR are based on generic |
183 on generic algebraic bit operations from theory |
184 algebraic bit operations from theory "HOL-Library.Bit_Operations". |
184 "HOL-Library.Bit_Operations". INCOMPATIBILITY. |
185 INCOMPATIBILITY. |
185 |
186 |
186 * Theory "HOL-Library.Word": Most operations on type word are set up for |
187 * Theory "Word": Most operations on type word are set up for transfer |
187 transfer and lifting. INCOMPATIBILITY. |
188 and lifting. INCOMPATIBILITY. |
188 |
189 |
189 * Theory "HOL-Library.Word": Generic type conversions. INCOMPATIBILITY, |
190 * Theory "Word": Generic type conversions. INCOMPATIBILITY, sometimes |
190 sometimes additional rewrite rules must be added to applications to get |
191 additional rewrite rules must be added to applications to get a |
191 a confluent system again. |
192 confluent system again. |
192 |
193 |
193 * Theory "HOL-Library.Word": Uniform polymorphic "mask" operation for |
194 * Theory "Word": Uniform polymorphic "mask" operation for both types int |
194 both types int and word. INCOMPATIBILITY. |
195 and word. INCOMPATIBILITY. |
195 |
196 |
196 * Theory "HOL-Library.Word": Syntax for signed compare operators has |
197 * Theory "Word": Syntax for signed compare operators has been |
197 been consolidated with syntax of regular compare operators. Minor |
198 consolidated with syntax of regular compare operators. Minor |
|
199 INCOMPATIBILITY. |
198 INCOMPATIBILITY. |
200 |
199 |
201 * Former session "HOL-Word": Various operations dealing with bit values |
200 * Former session "HOL-Word": Various operations dealing with bit values |
202 represented as reversed lists of bools are separated into theory |
201 represented as reversed lists of bools are separated into theory |
203 Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY. |
202 Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY. |