# HG changeset patch
# User paulson
# Date 959077944 -7200
# Node ID 4829556a56f898dfcc0f3d4daf84c003949a75b8
# Parent  1d3bf47a4ecc846efbe172c2fdd80bcb369b7309
declared sum_below

diff -r 1d3bf47a4ecc -r 4829556a56f8 src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Tue May 23 12:31:38 2000 +0200
+++ b/src/HOL/Arith.thy	Tue May 23 12:32:24 2000 +0200
@@ -26,4 +26,11 @@
   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) 
+primrec 
+  sum_below_0    "sum_below f 0 = 0"
+  sum_below_Suc  "sum_below f (Suc n) = f(n) + sum_below f n"
+
 end