equal
deleted
inserted
replaced
608 with all denominators that can be proved to be non-zero (in equations) |
608 with all denominators that can be proved to be non-zero (in equations) |
609 or positive/negative (in inequations). |
609 or positive/negative (in inequations). |
610 |
610 |
611 * Lemma collections ring_eq_simps, group_eq_simps and ring_distrib |
611 * Lemma collections ring_eq_simps, group_eq_simps and ring_distrib |
612 have been improved and renamed to ring_simps, group_simps and ring_distribs. |
612 have been improved and renamed to ring_simps, group_simps and ring_distribs. |
|
613 Removed lemmas field_xyz in Ring_and_Field |
|
614 because they were subsumed by lemmas xyz. |
|
615 INCOMPATIBILITY. |
613 |
616 |
614 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |
617 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |
615 when generating code. |
618 when generating code. |
616 |
619 |
617 * Library/Pretty_Char.thy: maps HOL characters on target language character literals |
620 * Library/Pretty_Char.thy: maps HOL characters on target language character literals |