changeset 32705 | 04ce6bb14d85 |
parent 32679 | 096306d7391d |
parent 32698 | be4b248616c0 |
child 32960 | 69916a850301 |
child 32988 | d1d4d7a08a66 |
--- a/src/HOL/Finite_Set.thy Thu Sep 24 19:14:18 2009 +0200 +++ b/src/HOL/Finite_Set.thy Fri Sep 25 09:50:31 2009 +0200 @@ -1565,9 +1565,7 @@ apply (rule finite_subset) prefer 2 apply assumption - apply auto - apply (rule setsum_cong) - apply auto + apply (auto simp add: sup_absorb2) done lemma setsum_right_distrib: