| changeset 37887 | 2ae085b07f2f |
| parent 37767 | a2b7a20d6ea3 |
| child 38621 | d6cb7e625d75 |
--- a/src/HOL/RealVector.thy Mon Jul 19 16:09:44 2010 +0200 +++ b/src/HOL/RealVector.thy Mon Jul 19 16:09:44 2010 +0200 @@ -30,7 +30,7 @@ qed lemma diff: "f (x - y) = f x - f y" -by (simp add: diff_def add minus) +by (simp add: add minus diff_minus) lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))" apply (cases "finite A")