# HG changeset patch
# User nipkow
# Date 1115053190 -7200
# Node ID b730b0edc0853d44062fff39137561d5bc78666d
# Parent  5df57194d064bed5916095e3069d4af5f5e34f6e
turned 2 lemmas into simp rules

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)