# HG changeset patch
# User paulson
# Date 959098911 -7200
# Node ID 23f85299689fda5a3a2ae8628e8ffe028c71f85e
# Parent  9660ca91828ccc9e5f3eac0060b4d1bf96d9fe44
finally sum_below is overloaded properly

diff -r 9660ca91828c -r 23f85299689f src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Tue May 23 18:19:06 2000 +0200
+++ b/src/HOL/Arith.thy	Tue May 23 18:21:51 2000 +0200
@@ -26,9 +26,8 @@
   mult_0   "0 * n = 0"
   mult_Suc "Suc m * n = n + (m * n)"
 
-(*We overload the constant for all + types, but unfortunately there's no
-  overloaded 0...*)
-consts sum_below :: [nat=>'a, nat] => ('a::plus) 
+(*We overload the constant for all + types*)
+consts sum_below :: "[nat=>'a, nat] => ('a::{zero,plus})"
 primrec 
   sum_below_0    "sum_below f 0 = 0"
   sum_below_Suc  "sum_below f (Suc n) = f(n) + sum_below f n"