*** empty log message ***
authornipkow
Sat, 01 Sep 2007 01:22:11 +0200
changeset 24507 ac22a2a67100
parent 24506 020db6ec334a
child 24508 c8b82fec6447
*** empty log message ***
NEWS
--- a/NEWS	Sat Sep 01 01:21:48 2007 +0200
+++ b/NEWS	Sat Sep 01 01:22:11 2007 +0200
@@ -847,7 +847,12 @@
 
 * Lemma "set_take_whileD" renamed to "set_takeWhileD"
 
-* new function "sgn" on ordered_idom, hence in particular on int and real.
+* function "sgn" is now overloaded and available on int, real, complex
+  (and other numeric types).
+  The details: new class "sgn" with function "sgn";
+  two possible defs of sgn in the classes sgn_if and sgn_div_norm
+  (as equational assumptions);
+  ordered_idom now also inherits from sgn_if - INCOMPATIBILITY.
 
 * New lemma collection field_simps (an extension of ring_simps)
   for manipulating (in)equations involving division. Multiplies