equal
deleted
inserted
replaced
234 nat_add_left_commute ~> add.left_commute |
234 nat_add_left_commute ~> add.left_commute |
235 nat_mult_assoc ~> mult.assoc |
235 nat_mult_assoc ~> mult.assoc |
236 nat_mult_commute ~> mult.commute |
236 nat_mult_commute ~> mult.commute |
237 eq_assoc ~> iff_assoc |
237 eq_assoc ~> iff_assoc |
238 eq_left_commute ~> iff_left_commute |
238 eq_left_commute ~> iff_left_commute |
|
239 |
|
240 INCOMPATIBILITY. |
|
241 |
|
242 * Removed collections add_ac and mult_ac. Prefer ac_simps instead, |
|
243 or specify rules (add|mult).(assoc|commute|left_commute) individually. |
|
244 |
|
245 INCOMPATIBILITY. |
239 |
246 |
240 * Qualified String.implode and String.explode. INCOMPATIBILITY. |
247 * Qualified String.implode and String.explode. INCOMPATIBILITY. |
241 |
248 |
242 * Simplifier: Enhanced solver of preconditions of rewrite rules can |
249 * Simplifier: Enhanced solver of preconditions of rewrite rules can |
243 now deal with conjunctions. For help with converting proofs, the old |
250 now deal with conjunctions. For help with converting proofs, the old |