# HG changeset patch
# User paulson
# Date 959186945 -7200
# Node ID 633e1682455c81076fd732e614957ce86a72af66
# Parent  b547482dd127f96cf9306bdda8f39413ed2ca0a1
setsum is now overloaded on plus_ac0

diff -r b547482dd127 -r 633e1682455c src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Wed May 24 18:48:22 2000 +0200
+++ b/src/HOL/Finite.thy	Wed May 24 18:49:05 2000 +0200
@@ -6,7 +6,7 @@
 Finite sets, their cardinality, and a fold functional.
 *)
 
-Finite = Divides + Power + Inductive +
+Finite = Divides + Power + Inductive + SetInterval +
 
 consts Finites :: 'a set set
 
@@ -57,8 +57,8 @@
 constdefs
    fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
   "fold f e A == @x. (A,x) : foldSet f e"
-  (* A frequent instance: *)
-   setsum :: ('a => nat) => 'a set => nat
+
+   setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)"
   "setsum f == fold (op+ o f) 0"
 
 locale LC =