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)
```