equal
deleted
inserted
replaced
594 eq_assoc ~> iff_assoc |
594 eq_assoc ~> iff_assoc |
595 eq_left_commute ~> iff_left_commute |
595 eq_left_commute ~> iff_left_commute |
596 |
596 |
597 INCOMPATIBILITY. |
597 INCOMPATIBILITY. |
598 |
598 |
599 * Removed collections add_ac and mult_ac. Prefer ac_simps instead, |
599 * Fact collections add_ac and mult_ac are considered old-fashined. |
600 or specify rules (add|mult).(assoc|commute|left_commute) individually. |
600 Prefer ac_simps instead, or specify rules |
601 |
601 (add|mult).(assoc|commute|left_commute) individually. |
602 INCOMPATIBILITY. |
|
603 |
602 |
604 * Elimination of fact duplicates: |
603 * Elimination of fact duplicates: |
605 equals_zero_I ~> minus_unique |
604 equals_zero_I ~> minus_unique |
606 diff_eq_0_iff_eq ~> right_minus_eq |
605 diff_eq_0_iff_eq ~> right_minus_eq |
607 nat_infinite ~> infinite_UNIV_nat |
606 nat_infinite ~> infinite_UNIV_nat |