--- 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
--- 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)