src/HOL/Algebra/IntRing.thy
 changeset 28524 644b62cf678f parent 28085 914183e229e9 child 28823 dcbef866c9e2
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Oct 07 16:07:40 2008 +0200
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Oct 07 16:07:50 2008 +0200
1.3 @@ -118,7 +118,7 @@
1.4  qed
1.5
1.6  interpretation int: comm_monoid ["\<Z>"]
1.7 -  where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
1.8 +  where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
1.9  proof -
1.10    -- "Specification"
1.11    show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
1.12 @@ -128,7 +128,7 @@
1.13    { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
1.14    note mult = this
1.15    have one: "one \<Z> = 1" by (simp add: int_ring_def)
1.16 -  show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
1.17 +  show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
1.18    proof (cases "finite A")
1.19      case True then show ?thesis proof induct
1.20        case empty show ?case by (simp add: one)
1.21 @@ -143,7 +143,7 @@
1.22  interpretation int: abelian_monoid ["\<Z>"]
1.23    where "zero \<Z> = 0"
1.24      and "add \<Z> x y = x + y"
1.25 -    and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
1.26 +    and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
1.27  proof -
1.28    -- "Specification"
1.29    show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
1.30 @@ -153,7 +153,7 @@
1.31    { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }