equal
deleted
inserted
replaced
74 "bintrunc" and "max_word" are now mere input abbreviations. |
74 "bintrunc" and "max_word" are now mere input abbreviations. |
75 Minor INCOMPATIBILITY. |
75 Minor INCOMPATIBILITY. |
76 |
76 |
77 * Session HOL-Word: Theory Z2 is not used any longer. |
77 * Session HOL-Word: Theory Z2 is not used any longer. |
78 Minor INCOMPATIBILITY. |
78 Minor INCOMPATIBILITY. |
|
79 |
|
80 * Session HOL-Word: Operations lsb, msb and set_bit are separated |
|
81 into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. |
|
82 INCOMPATIBILITY. |
79 |
83 |
80 * Simproc defined_all and rewrite rule subst_all perform |
84 * Simproc defined_all and rewrite rule subst_all perform |
81 more aggressive substitution with variables from assumptions. |
85 more aggressive substitution with variables from assumptions. |
82 INCOMPATIBILITY, use something like |
86 INCOMPATIBILITY, use something like |
83 "supply subst_all [simp del] [[simproc del: defined_all]]" |
87 "supply subst_all [simp del] [[simproc del: defined_all]]" |