1.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -66,7 +66,7 @@
     1.4      apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
     1.5      have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
     1.6      thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
     1.7 -      unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def
     1.8 +      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
     1.9        unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
    1.10    note lem3 = this[rule_format]
    1.11    have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto