changeset 8970 | 3ac901561f33 |
parent 8939 | 23f85299689f |
child 9436 | 62bb04ab4b01 |
--- 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