src/HOL/Algebra/Ring.thy
changeset 22265 3c5c6bdf61de
parent 21896 9a7949815a84
child 23350 50c5b0912a0c
     1.1 --- a/src/HOL/Algebra/Ring.thy	Wed Feb 07 17:30:53 2007 +0100
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Feb 07 17:32:52 2007 +0100
     1.3 @@ -552,7 +552,7 @@
     1.4  lemma (in cring) finsum_ldistr:
     1.5    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
     1.6     finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
     1.7 -proof (induct set: Finites)
     1.8 +proof (induct set: finite)
     1.9    case empty then show ?case by simp
    1.10  next
    1.11    case (insert x F) then show ?case by (simp add: Pi_def l_distr)
    1.12 @@ -561,7 +561,7 @@
    1.13  lemma (in cring) finsum_rdistr:
    1.14    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    1.15     a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
    1.16 -proof (induct set: Finites)
    1.17 +proof (induct set: finite)
    1.18    case empty then show ?case by simp
    1.19  next
    1.20    case (insert x F) then show ?case by (simp add: Pi_def r_distr)
    1.21 @@ -745,7 +745,7 @@
    1.22  lemma (in ring_hom_cring) hom_finsum [simp]:
    1.23    "[| finite A; f \<in> A -> carrier R |] ==>
    1.24    h (finsum R f A) = finsum S (h o f) A"
    1.25 -proof (induct set: Finites)
    1.26 +proof (induct set: finite)
    1.27    case empty then show ?case by simp
    1.28  next
    1.29    case insert then show ?case by (simp add: Pi_def)
    1.30 @@ -754,7 +754,7 @@
    1.31  lemma (in ring_hom_cring) hom_finprod:
    1.32    "[| finite A; f \<in> A -> carrier R |] ==>
    1.33    h (finprod R f A) = finprod S (h o f) A"
    1.34 -proof (induct set: Finites)
    1.35 +proof (induct set: finite)
    1.36    case empty then show ?case by simp
    1.37  next
    1.38    case insert then show ?case by (simp add: Pi_def)