src/HOL/Real_Vector_Spaces.thy
changeset 60307 75e1aa7a450e
parent 60303 00c06f1315d0
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu May 28 10:18:46 2015 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu May 28 14:33:35 2015 +0100
     1.3 @@ -1222,6 +1222,9 @@
     1.4  lemma norm_conv_dist: "norm x = dist x 0"
     1.5    unfolding dist_norm by simp
     1.6  
     1.7 +lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
     1.8 +  by (simp_all add: dist_norm)
     1.9 +  
    1.10  subsection {* Bounded Linear and Bilinear Operators *}
    1.11  
    1.12  locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +