# HG changeset patch
# User huffman
# Date 1312911727 25200
# Node ID ce44e70d0c474d60557c4c613dcde87dd8384713
# Parent  230a8665c919951e05cd79939354ea1ad4d50562
avoid duplicate rewrite warnings

diff -r 230a8665c919 -r ce44e70d0c47 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Tue Aug 09 10:30:00 2011 -0700
+++ b/src/HOL/Library/Inner_Product.thy	Tue Aug 09 10:42:07 2011 -0700
@@ -123,8 +123,7 @@
         unfolding power2_sum power2_norm_eq_inner
         by (simp add: inner_add inner_commute)
       show "0 \<le> norm x + norm y"
-        unfolding norm_eq_sqrt_inner
-        by (simp add: add_nonneg_nonneg)
+        unfolding norm_eq_sqrt_inner by simp
     qed
   have "sqrt (a\<twosuperior> * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
     by (simp add: real_sqrt_mult_distrib)
@@ -217,7 +216,7 @@
   show "inner (scaleR r x) y = r * inner x y"
     unfolding inner_complex_def by (simp add: right_distrib)
   show "0 \<le> inner x x"
-    unfolding inner_complex_def by (simp add: add_nonneg_nonneg)
+    unfolding inner_complex_def by simp
   show "inner x x = 0 \<longleftrightarrow> x = 0"
     unfolding inner_complex_def
     by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
diff -r 230a8665c919 -r ce44e70d0c47 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:30:00 2011 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:42:07 2011 -0700
@@ -453,9 +453,9 @@
   assumes x: "0 \<le> x" and y: "0 \<le> y"
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
-apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
+apply (simp add: real_sum_squared_expand x y)
 apply (simp add: mult_nonneg_nonneg x y)
-apply (simp add: add_nonneg_nonneg x y)
+apply (simp add: x y)
 done
 
 lemma bounded_linear_Pair: