# HG changeset patch
# User huffman
# Date 1235263902 28800
# Node ID 49f603f92c4726af753d07b808b3dafec916f010
# Parent  b8ddd7667eede528abffabd44fc7c18ea720171c
fix spelling

diff -r b8ddd7667eed -r 49f603f92c47 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Sat Feb 21 15:39:59 2009 -0800
+++ b/src/HOL/Library/Inner_Product.thy	Sat Feb 21 16:51:42 2009 -0800
@@ -65,7 +65,7 @@
 lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"
   by (simp add: norm_eq_sqrt_inner)
 
-lemma Cauchy_Schwartz_ineq:
+lemma Cauchy_Schwarz_ineq:
   "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
 proof (cases)
   assume "y = 0"
@@ -86,11 +86,11 @@
     by (simp add: pos_divide_le_eq y)
 qed
 
-lemma Cauchy_Schwartz_ineq2:
+lemma Cauchy_Schwarz_ineq2:
   "\<bar>inner x y\<bar> \<le> norm x * norm y"
 proof (rule power2_le_imp_le)
   have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
-    using Cauchy_Schwartz_ineq .
+    using Cauchy_Schwarz_ineq .
   thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
     by (simp add: power_mult_distrib power2_norm_eq_inner)
   show "0 \<le> norm x * norm y"
@@ -108,7 +108,7 @@
   show "norm (x + y) \<le> norm x + norm y"
     proof (rule power2_le_imp_le)
       have "inner x y \<le> norm x * norm y"
-        by (rule order_trans [OF abs_ge_self Cauchy_Schwartz_ineq2])
+        by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
       thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
         unfolding power2_sum power2_norm_eq_inner
         by (simp add: inner_distrib inner_commute)
@@ -140,7 +140,7 @@
   show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   proof
     show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
-      by (simp add: Cauchy_Schwartz_ineq2)
+      by (simp add: Cauchy_Schwarz_ineq2)
   qed
 qed