src/HOL/NatArith.thy

 fun add_arith cs = cs addafter ("arith_tac", arith_tac);
 TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
-(*
-subsection {* Generic summation indexed over natural numbers *}
-
-consts
-  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
-primrec
-  "Summation f 0 = 0"
-  "Summation f (Suc n) = Summation f n + f n"
-
-syntax
-  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
-translations
-  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
-
-theorem Summation_step:
-    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
-  by (induct n) simp_all
-*)
 end