# HG changeset patch
# User berghofe
# Date 1120219273 -7200
# Node ID 62dff56b43d3fc0693122d2611dece708694e7c4
# Parent  1ed737a98198b3419404d2b9f804ebc571ffff6f
Tuned finsum_cong to allow that premises are simplified more eagerly.

diff -r 1ed737a98198 -r 62dff56b43d3 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Fri Jul 01 13:57:53 2005 +0200
+++ b/src/HOL/Algebra/CRing.thy	Fri Jul 01 14:01:13 2005 +0200
@@ -277,10 +277,10 @@
     simplified monoid_record_simps])
 
 lemma (in abelian_monoid) finsum_cong:
-  "[| A = B; f : B -> carrier G = True;
-      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
+  "[| A = B; f : B -> carrier G;
+      !!i. i : B =simp=> f i = g i |] ==> finsum G f A = finsum G g B"
   by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
-    simplified monoid_record_simps]) auto
+    simplified monoid_record_simps]) (auto simp add: simp_implies_def)
 
 text {*Usually, if this rule causes a failed congruence proof error,
    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.