# HG changeset patch
# User huffman
# Date 1243996964 25200
# Node ID b67a3ac4882dd4cdfb8c4cf9adceb0bf44eb9204
# Parent  8f3921c5979278b58b8134e5de3110a31b471e25
generalize lemma norm_triangle_sub

diff -r 8f3921c59792 -r b67a3ac4882d src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 19:29:18 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 19:42:44 2009 -0700
@@ -939,8 +939,11 @@
   using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
   by (simp add: real_abs_def dot_rneg)
 
-lemma norm_triangle_sub: "norm (x::real ^'n::finite) <= norm(y) + norm(x - y)"
+lemma norm_triangle_sub:
+  fixes x y :: "'a::real_normed_vector"
+  shows "norm x \<le> norm y  + norm (x - y)"
   using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
+
 lemma norm_triangle_le: "norm(x::real ^'n::finite) + norm y <= e ==> norm(x + y) <= e"
   by (metis order_trans norm_triangle_ineq)
 lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e"