| changeset 14329 | ff3210fe968f |
| parent 14309 | f508492af9b4 |
| child 14352 | a8b1a44d8264 |
--- a/src/HOL/Hyperreal/HyperArith.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/HyperArith.thy Thu Dec 25 22:48:32 2003 +0100 @@ -4,6 +4,16 @@ setup hypreal_arith_setup +text{*Used once in NSA*} +lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" +apply arith +done + +ML +{* +val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; +*} + subsubsection{*Division By @{term 1} and @{term "-1"}*} lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)"