diff -r 0e4906ccf280 -r d4707b99e631 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Fri Jun 12 11:23:37 2009 -0700
+++ b/src/HOL/RealVector.thy	Fri Jun 12 11:39:23 2009 -0700
@@ -116,11 +116,11 @@
   thus "a = b" by (simp only: right_minus_eq)
 qed
 
-lemma scale_cancel_left:
+lemma scale_cancel_left [simp]:
   "scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0"
 by (auto intro: scale_left_imp_eq)
 
-lemma scale_cancel_right:
+lemma scale_cancel_right [simp]:
   "scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0"
 by (auto intro: scale_right_imp_eq)
 
@@ -571,7 +571,7 @@
   assumes norm_ge_zero [simp]: "0 \<le> norm x"
   and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
   and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
-  and norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
+  and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
 
 class real_normed_algebra = real_algebra + real_normed_vector +
   assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
@@ -701,7 +701,7 @@
 
 lemma norm_of_real [simp]:
   "norm (of_real r :: 'a::real_normed_algebra_1) = \<bar>r\<bar>"
-unfolding of_real_def by (simp add: norm_scaleR)
+unfolding of_real_def by simp
 
 lemma norm_number_of [simp]:
   "norm (number_of w::'a::{number_ring,real_normed_algebra_1})
@@ -866,7 +866,7 @@
 
 lemma norm_sgn:
   "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)"
-by (simp add: sgn_div_norm norm_scaleR)
+by (simp add: sgn_div_norm)
 
 lemma sgn_zero [simp]: "sgn(0::'a::real_normed_vector) = 0"
 by (simp add: sgn_div_norm)
@@ -879,7 +879,7 @@
 
 lemma sgn_scaleR:
   "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
-by (simp add: sgn_div_norm norm_scaleR mult_ac)
+by (simp add: sgn_div_norm mult_ac)
 
 lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
 by (simp add: sgn_div_norm)
@@ -1047,8 +1047,7 @@
 apply (rule scaleR_right_distrib)
 apply simp
 apply (rule scaleR_left_commute)
-apply (rule_tac x="1" in exI)
-apply (simp add: norm_scaleR)
+apply (rule_tac x="1" in exI, simp)
 done
 
 interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"