doc-src/Tutorial/Misc/natsum
author paulson
Mon, 05 Mar 2001 15:25:11 +0100
changeset 11193 851c90b23a9e
parent 5377 efb799c5ed3c
permissions -rw-r--r--
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp

consts sum :: nat => nat
primrec
"sum 0 = 0"
"sum (Suc n) = Suc n + sum n"