# HG changeset patch
# User paulson
# Date 959260360 -7200
# Node ID 3ac901561f335d937e4c7ebc132915b6db18467d
# Parent  23c6e0ca00860b9b10e3060025b445a936231d61
deleted sum_below: no need for it with setsum and lessThan

diff -r 23c6e0ca0086 -r 3ac901561f33 src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Thu May 25 15:12:00 2000 +0200
+++ b/src/HOL/Arith.thy	Thu May 25 15:12:40 2000 +0200
@@ -26,10 +26,4 @@
   mult_0   "0 * n = 0"
   mult_Suc "Suc m * n = n + (m * n)"
 
-(*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"
-
 end