diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/RealVector.thy
--- 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")