src/HOL/Finite_Set.thy
changeset 32683 7c1fe854ca6a
parent 32437 66f1a0dfe7d9
child 32697 72e8608dce54
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Sep 18 14:09:38 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sat Sep 19 07:38:03 2009 +0200
     1.3 @@ -1566,8 +1566,6 @@
     1.4    prefer 2
     1.5    apply assumption
     1.6    apply auto
     1.7 -  apply (rule setsum_cong)
     1.8 -  apply auto
     1.9  done
    1.10  
    1.11  lemma setsum_right_distrib: