* HOL/Library: a collection of generic theories to be used together
with main HOL; the theory loader path already includes this directory
by default; the following existing theories have been moved here:
HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
(as While_Combinator);
consts sum :: nat => nat
primrec
"sum 0 = 0"
"sum (Suc n) = Suc n + sum n"