src/HOL/Hyperreal/Series.thy
changeset 11701 3d51fbf81c17
parent 10751 a81ea5d3dd41
child 12018 ec054019c910
--- a/src/HOL/Hyperreal/Series.thy	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Fri Oct 05 21:52:39 2001 +0200
@@ -9,8 +9,8 @@
 
 consts sumr :: "[nat,nat,(nat=>real)] => real"
 primrec
-   sumr_0   "sumr m 0 f = #0"
-   sumr_Suc "sumr m (Suc n) f = (if n < m then #0 
+   sumr_0   "sumr m 0 f = Numeral0"
+   sumr_Suc "sumr m (Suc n) f = (if n < m then Numeral0 
                                else sumr m n f + f(n))"
 
 constdefs