# HG changeset patch
# User chaieb
# Date 1234199329 0
# Node ID 4ac95212efcc2701efd24d92763b4542fd9d8f9e
# Parent  4bb780545478e2d074b83aeb263243ea28b91442
fixed proof -- removed unnecessary sorry

diff -r 4bb780545478 -r 4ac95212efcc src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Feb 09 16:57:10 2009 +0000
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Feb 09 17:08:49 2009 +0000
@@ -3986,8 +3986,7 @@
 	apply (rule setsum_0')
 	apply clarsimp
 	apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
-	by auto
-      have "orthogonal x y" using xa ya sorry}
+	by auto}
     moreover
     {assume xa: "x \<in> C" and ya: "y \<in> C" 
       have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast}