# HG changeset patch
# User huffman
# Date 1272517375 25200
# Node ID 4fa71a69d5b2765e4aeeb132974caeb2fcfd0faa
# Parent  f2faab7b46e7cc33f40abfe6e0bfe292e8897a64
remove redundant lemma norm_0

diff -r f2faab7b46e7 -r 4fa71a69d5b2 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 28 21:39:14 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 28 22:02:55 2010 -0700
@@ -2110,7 +2110,7 @@
         unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def])
       case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
         apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
-        unfolding norm_0 scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof-
+        unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof-
         fix e and x::"real^'n" assume as:"norm x < e / B" "0 < norm x" "0<e"
         hence "surf (pi x) \<in> frontier s" using pi(1)[of x] unfolding surf(5)[THEN sym] by auto
         hence "norm (surf (pi x)) \<le> B" using B fs by auto
diff -r f2faab7b46e7 -r 4fa71a69d5b2 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- 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)