| changeset 35216 | 7641e8d831d2 |
| parent 31586 | d4707b99e631 |
| child 36349 | 39be26d1bc28 |
--- a/src/HOL/RealVector.thy Thu Feb 18 13:29:59 2010 -0800 +++ b/src/HOL/RealVector.thy Thu Feb 18 14:21:44 2010 -0800 @@ -268,7 +268,7 @@ by (induct n) simp_all lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)" -by (simp add: of_real_def scaleR_cancel_right) +by (simp add: of_real_def) lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]