src/HOL/ex/NatSum.thy
changeset 8356 14d89313c66c
parent 5184 9b8547a9496a
child 8836 32fe62227ff0
--- a/src/HOL/ex/NatSum.thy	Wed Mar 08 16:17:10 2000 +0100
+++ b/src/HOL/ex/NatSum.thy	Wed Mar 08 16:24:46 2000 +0100
@@ -6,7 +6,7 @@
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
 *)
 
-NatSum = Arith +
+NatSum = Main +
 consts sum     :: [nat=>nat, nat] => nat
 primrec 
   "sum f 0 = 0"