--- 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.