equal
deleted
inserted
replaced
845 [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, |
845 [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, |
846 and for uniformity. INCOMPATIBILITY |
846 and for uniformity. INCOMPATIBILITY |
847 |
847 |
848 * Lemma "set_take_whileD" renamed to "set_takeWhileD" |
848 * Lemma "set_take_whileD" renamed to "set_takeWhileD" |
849 |
849 |
850 * new function "sgn" on ordered_idom, hence in particular on int and real. |
850 * function "sgn" is now overloaded and available on int, real, complex |
|
851 (and other numeric types). |
|
852 The details: new class "sgn" with function "sgn"; |
|
853 two possible defs of sgn in the classes sgn_if and sgn_div_norm |
|
854 (as equational assumptions); |
|
855 ordered_idom now also inherits from sgn_if - INCOMPATIBILITY. |
851 |
856 |
852 * New lemma collection field_simps (an extension of ring_simps) |
857 * New lemma collection field_simps (an extension of ring_simps) |
853 for manipulating (in)equations involving division. Multiplies |
858 for manipulating (in)equations involving division. Multiplies |
854 with all denominators that can be proved to be non-zero (in equations) |
859 with all denominators that can be proved to be non-zero (in equations) |
855 or positive/negative (in inequations). |
860 or positive/negative (in inequations). |