Mercurial Mercurial > repos > Old_HOL / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ex/natsum.thy
author nipkow
Fri, 02 Dec 1994 16:09:49 +0100
changeset 195 df6b3bd14dcb
parent 68 acad709cad5d
permissions -rw-r--r--
Moved HOL/List to HOL/ex/SList (strict list). Modified sons on (S)List accordingly.

(*  Title: 	HOL/ex/natsum.thy
    ID:         $Id$
    Author: 	Tobias Nipkow
    Copyright   1994 TU Muenchen

A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
*)

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)"
end
Old_HOL