diff -r 7cf01ece66e4 -r dcfb33c26f50 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
@@ -137,17 +137,17 @@
 end
 *} "lift trivial vector statements to real arith statements"
 
-lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
-lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
+lemma vec_0[simp]: "vec 0 = 0" by vector
+lemma vec_1[simp]: "vec 1 = 1" by vector
 
 lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
 
 lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
 
-lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
-lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
-lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
-lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
+lemma vec_add: "vec(x + y) = vec x + vec y"  by vector
+lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
+lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
+lemma vec_neg: "vec(- x) = - vec x " by vector
 
 lemma vec_setsum:
   assumes "finite S"
@@ -164,7 +164,7 @@
 text{* Obvious "component-pushing". *}
 
 lemma vec_component [simp]: "vec x $ i = x"
-  by (vector vec_def)
+  by vector
 
 lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
   by vector
@@ -330,7 +330,7 @@
   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
   shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
   using setsum_norm_allsubsets_bound[OF assms]
-  by (simp add: DIM_cart Basis_real_def)
+  by simp
 
 subsection {* Matrix operations *}