src/HOL/Library/Euclidean_Space.thy
changeset 32685 29e4e567b5f4
parent 32456 341c83339aeb
child 32698 be4b248616c0
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sat Sep 19 07:38:11 2009 +0200
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 11:01:39 2009 +0200
     1.3 @@ -3649,10 +3649,7 @@
     1.4      from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     1.5      have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
     1.6        unfolding cond_value_iff cond_application_beta
     1.7 -      apply (simp add: cond_value_iff cong del: if_weak_cong)
     1.8 -      apply (rule setsum_cong)
     1.9 -      apply auto
    1.10 -      done
    1.11 +      by (simp add: cond_value_iff cong del: if_weak_cong)
    1.12      hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
    1.13      hence "y \<in> ?rhs" by auto}
    1.14    moreover