--- a/src/HOL/SetInterval.thy Mon May 02 18:46:52 2005 +0200
+++ b/src/HOL/SetInterval.thy Mon May 02 18:59:50 2005 +0200
@@ -617,11 +617,11 @@
by (simp add:lessThan_Suc)
*)
-lemma setsum_cl_ivl_Suc:
+lemma setsum_cl_ivl_Suc[simp]:
"setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
by (auto simp:add_ac atLeastAtMostSuc_conv)
-lemma setsum_op_ivl_Suc:
+lemma setsum_op_ivl_Suc[simp]:
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
by (auto simp:add_ac atLeastLessThanSuc)