182 |
182 |
183 * Combinator "Fun.swap" resolved into a mere input abbreviation in |
183 * Combinator "Fun.swap" resolved into a mere input abbreviation in |
184 separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. |
184 separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. |
185 |
185 |
186 * Infix syntax for bit operations AND, OR, XOR is now organized in |
186 * Infix syntax for bit operations AND, OR, XOR is now organized in |
187 bundle bit_operations_syntax. INCOMPATIBILITY. |
187 bundle bit_operations_syntax. INCOMPATIBILITY. |
188 |
188 |
189 * Bit operations set_bit, unset_bit and flip_bit are now class |
189 * Bit operations set_bit, unset_bit and flip_bit are now class |
190 operations. INCOMPATIBILITY. |
190 operations. INCOMPATIBILITY. |
|
191 |
|
192 * Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY. |
191 |
193 |
192 * Abbreviation "max_word" has been moved to session Word_Lib in the AFP, |
194 * Abbreviation "max_word" has been moved to session Word_Lib in the AFP, |
193 as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", |
195 as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", |
194 "setBit", "clearBit". See there further the changelog in theory Guide. |
196 "setBit", "clearBit". See there further the changelog in theory Guide. |
195 INCOMPATIBILITY. |
197 INCOMPATIBILITY. |
196 |
198 |
197 * New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3, |
199 * New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3, |
198 min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor |
200 min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor |
199 INCOMPATIBILITY. |
201 INCOMPATIBILITY. |
200 |
202 |
201 * Sledgehammer: |
203 * Sledgehammer: |
202 - Removed legacy "lam_lifting" (synonym for "liftinng") from option |
204 - Removed legacy "lam_lifting" (synonym for "liftinng") from option |
203 "lam_trans". Minor INCOMPATIBILITY. |
205 "lam_trans". Minor INCOMPATIBILITY. |
207 using combinators, but the combinators are kept opaque, i.e. without |
209 using combinators, but the combinators are kept opaque, i.e. without |
208 definitions. |
210 definitions. |
209 |
211 |
210 * Metis: |
212 * Metis: |
211 - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. |
213 - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. |
|
214 |
212 |
215 |
213 *** ML *** |
216 *** ML *** |
214 |
217 |
215 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on |
218 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on |
216 the given ML expression, in contrast to functions "try" and "can" that |
219 the given ML expression, in contrast to functions "try" and "can" that |