*** empty log message ***
authornipkow
Thu, 30 Aug 2007 21:44:29 +0200
changeset 24492 de3fd08bb41c
parent 24491 8d194c9198ae
child 24493 d4380e9b287b
*** empty log message ***
NEWS
--- 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)