src/HOL/Algebra/FiniteProduct.thy
changeset 41433 1b8ff770f02c
parent 40786 0a54cfc9add3
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Jan 06 17:51:56 2011 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jan 06 21:06:17 2011 +0100
     1.3 @@ -450,9 +450,9 @@
     1.4  
     1.5  lemma finprod_cong:
     1.6    "[| A = B; f \<in> B -> carrier G = True;
     1.7 -      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
     1.8 +      !!i. i \<in> B =simp=> f i = g i |] ==> finprod G f A = finprod G g B"
     1.9    (* This order of prems is slightly faster (3%) than the last two swapped. *)
    1.10 -  by (rule finprod_cong') force+
    1.11 +  by (rule finprod_cong') (auto simp add: simp_implies_def)
    1.12  
    1.13  text {*Usually, if this rule causes a failed congruence proof error,
    1.14    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.