# HG changeset patch
# User huffman
# Date 1179162890 -7200
# Node ID a6812b6a36a5456b97deac2fba255d3bb5791154
# Parent  b5910e3dec4cba2c8866e57aa7b7c01eadecdf1b
root and sqrt on negative inputs

diff -r b5910e3dec4c -r a6812b6a36a5 NEWS
--- a/NEWS	Mon May 14 18:48:24 2007 +0200
+++ b/NEWS	Mon May 14 19:14:50 2007 +0200
@@ -868,6 +868,12 @@
 feature is used only for decision, for compatibility with arith. This
 means a goal is either solved or left unchanged, no simplification.
 
+* Hyperreal: Functions root and sqrt are now defined on negative real
+inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x.
+Nonnegativity side conditions have been removed from many lemmas, so
+that more subgoals may now be solved by simplification; potential
+INCOMPATIBILITY.
+
 * Real: New axiomatic classes formalize real normed vector spaces and
 algebras, using new overloaded constants scaleR :: real => 'a => 'a
 and norm :: 'a => real.