# HG changeset patch
# User paulson
# Date 959260522 -7200
# Node ID a76f80911eb9d36cd9c1871fe435e8ed9b45f7da
# Parent  ac448cd4345201afd29cea0606298e0a413e8347
sum_below moved here from Arith

diff -r ac448cd43452 -r a76f80911eb9 src/HOL/UNITY/AllocBase.thy
--- a/src/HOL/UNITY/AllocBase.thy	Thu May 25 15:14:39 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.thy	Thu May 25 15:15:22 2000 +0200
@@ -21,4 +21,10 @@
   "tokens [] = 0"
   "tokens (x#xs) = x + tokens xs"
 
+(*Or could be setsum...(lessThan n)*)
+consts sum_below :: "[nat=>'a, nat] => ('a::plus_ac0)"
+primrec 
+  sum_below_0    "sum_below f 0 = 0"
+  sum_below_Suc  "sum_below f (Suc n) = f(n) + sum_below f n"
+
 end