HOL/ROOT/HOL_dup_cs: removed as obsolete
HOL/ROOT: now passes "classical" to Classical_Fun
HOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac
(* Title: HOL/ex/sum.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1994 TU Muenchen
A summation operator
*)
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