# HG changeset patch
# User paulson
# Date 864204921 -7200
# Node ID eca2a3634acde4576a9e61f7549941c449bf5f7c
# Parent  012c43174664a99044f308bbf80dcb1be5122e2e
Function "sum" now defined using primrec

diff -r 012c43174664 -r eca2a3634acd src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Wed May 21 10:54:10 1997 +0200
+++ b/src/HOL/ex/NatSum.ML	Wed May 21 10:55:21 1997 +0200
@@ -3,11 +3,12 @@
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
-Summing natural numbers, squares and cubes. Could be continued...
+Summing natural numbers, squares and cubes.  Could be continued...
+Demonstrates permutative rewriting.
 *)
 
-Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
-Addsimps [add_mult_distrib,add_mult_distrib2];
+Addsimps add_ac;
+Addsimps [add_mult_distrib, add_mult_distrib2];
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
 goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
diff -r 012c43174664 -r eca2a3634acd src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Wed May 21 10:54:10 1997 +0200
+++ b/src/HOL/ex/NatSum.thy	Wed May 21 10:55:21 1997 +0200
@@ -8,6 +8,8 @@
 
 NatSum = Arith +
 consts sum     :: [nat=>nat, nat] => nat
-rules  sum_0      "sum f 0 = 0"
-       sum_Suc    "sum f (Suc n) = f(n) + sum f n"
+primrec "sum" nat 
+  "sum f 0 = 0"
+  "sum f (Suc n) = f(n) + sum f n"
+
 end