--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 21:39:14 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 22:02:55 2010 -0700
@@ -701,13 +701,6 @@
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)