src/HOL/Multivariate_Analysis/Euclidean_Space.thy

   using sqrt_divide_self_eq[of x]
   apply (simp add: inverse_eq_divide field_simps)
   done
 
 text{* Hence derive more interesting properties of the norm. *}
-
-text {*
-  This type-specific version is only here
-  to make @{text normarith.ML} happy.
-*}
-lemma norm_0: "norm (0::real ^ _) = 0"
-  by (rule norm_zero)
 
 lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"
   by (simp add: norm_vector_def setL2_right_distrib abs_mult)
 
 lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"