
diff -r 5df57194d064 -r b730b0edc085 src/HOL/SetInterval.thy
--- 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)
 




