| changeset 14321 | 55c688d2eefa |
| parent 14308 | c0489217deb2 |
| child 14329 | ff3210fe968f |
--- a/src/HOL/Real/RealArith.thy Tue Dec 23 14:45:47 2003 +0100 +++ b/src/HOL/Real/RealArith.thy Tue Dec 23 14:46:08 2003 +0100 @@ -47,7 +47,7 @@ Addsimps [symmetric real_diff_def] *) -subsubsection{*Division By @{term 1} and @{term "-1"}*} +subsubsection{*Division By @{term "-1"}*} lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)" by simp