author | huffman |

Mon May 14 19:14:50 2007 +0200 (2007-05-14) | |

changeset 22971 | a6812b6a36a5 |

parent 22970 | b5910e3dec4c |

child 22972 | 3e96b98d37c6 |

root and sqrt on negative inputs

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