| changeset 72000 | 379d0c207c29 |
| parent 71989 | bad75618fb82 |
| child 72001 | 3e08311ada8e |
--- a/NEWS Sun Jul 05 11:06:09 2020 +0200 +++ b/NEWS Mon Jul 06 10:47:30 2020 +0000 @@ -77,6 +77,10 @@ * Session HOL-Word: Theory Z2 is not used any longer. Minor INCOMPATIBILITY. +* Session HOL-Word: Operations lsb, msb and set_bit are separated +into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. +INCOMPATIBILITY. + * Simproc defined_all and rewrite rule subst_all perform more aggressive substitution with variables from assumptions. INCOMPATIBILITY, use something like