author | nipkow |
Thu, 30 Aug 2007 21:44:29 +0200 | |
changeset 24492 | de3fd08bb41c |
parent 24491 | 8d194c9198ae |
child 24493 | d4380e9b287b |
--- a/NEWS Thu Aug 30 21:43:31 2007 +0200 +++ b/NEWS Thu Aug 30 21:44:29 2007 +0200 @@ -847,6 +847,8 @@ * Lemma "set_take_whileD" renamed to "set_takeWhileD" +* new function "sgn" on ordered_idom, hence in particular on int and real. + * New lemma collection field_simps (an extension of ring_simps) for manipulating (in)equations involving division. Multiplies with all denominators that can be proved to be non-zero (in equations)