src/HOL/Algebra/IntRing.thy
changeset 64272 f76b6dda2e56
parent 64267 b9a1486e79be
child 65417 fc41a5650fb1
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Mon Oct 17 14:37:32 2016 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Mon Oct 17 17:33:07 2016 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  qed
     1.5  
     1.6  interpretation int: comm_monoid \<Z>
     1.7 -  rewrites "finprod \<Z> f A = setprod f A"
     1.8 +  rewrites "finprod \<Z> f A = prod f A"
     1.9  proof -
    1.10    \<comment> "Specification"
    1.11    show "comm_monoid \<Z>" by standard auto
    1.12 @@ -83,7 +83,7 @@
    1.13    { fix x y have "mult \<Z> x y = x * y" by simp }
    1.14    note mult = this
    1.15    have one: "one \<Z> = 1" by simp
    1.16 -  show "finprod \<Z> f A = setprod f A"
    1.17 +  show "finprod \<Z> f A = prod f A"
    1.18      by (induct A rule: infinite_finite_induct, auto)
    1.19  qed
    1.20