src/HOL/Hyperreal/Series.thy
changeset 12018 ec054019c910
parent 11701 3d51fbf81c17
child 14416 1f256287d4f0
--- a/src/HOL/Hyperreal/Series.thy	Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Fri Nov 02 17:55:24 2001 +0100
@@ -9,8 +9,8 @@
 
 consts sumr :: "[nat,nat,(nat=>real)] => real"
 primrec
-   sumr_0   "sumr m 0 f = Numeral0"
-   sumr_Suc "sumr m (Suc n) f = (if n < m then Numeral0 
+   sumr_0   "sumr m 0 f = 0"
+   sumr_Suc "sumr m (Suc n) f = (if n < m then 0 
                                else sumr m n f + f(n))"
 
 constdefs