fixed proof -- removed unnecessary sorry
authorchaieb
Mon Feb 09 17:08:49 2009 +0000 (2009-02-09)
changeset 298444ac95212efcc
parent 29843 4bb780545478
child 29845 5ef75225c9c2
fixed proof -- removed unnecessary sorry
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Feb 09 16:57:10 2009 +0000
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Feb 09 17:08:49 2009 +0000
     1.3 @@ -3986,8 +3986,7 @@
     1.4  	apply (rule setsum_0')
     1.5  	apply clarsimp
     1.6  	apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
     1.7 -	by auto
     1.8 -      have "orthogonal x y" using xa ya sorry}
     1.9 +	by auto}
    1.10      moreover
    1.11      {assume xa: "x \<in> C" and ya: "y \<in> C" 
    1.12        have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast}