summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 22971 | a6812b6a36a5 |

parent 22965 | b81bbe298406 |

child 22972 | 3e96b98d37c6 |

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.