turned 2 lemmas into simp rules
authornipkow
Mon May 02 18:59:50 2005 +0200 (2005-05-02)
changeset 15911b730b0edc085
parent 15910 5df57194d064
child 15912 47aa1a8fcdc9
turned 2 lemmas into simp rules
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Mon May 02 18:46:52 2005 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Mon May 02 18:59:50 2005 +0200
     1.3 @@ -617,11 +617,11 @@
     1.4  by (simp add:lessThan_Suc)
     1.5  *)
     1.6  
     1.7 -lemma setsum_cl_ivl_Suc:
     1.8 +lemma setsum_cl_ivl_Suc[simp]:
     1.9    "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
    1.10  by (auto simp:add_ac atLeastAtMostSuc_conv)
    1.11  
    1.12 -lemma setsum_op_ivl_Suc:
    1.13 +lemma setsum_op_ivl_Suc[simp]:
    1.14    "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
    1.15  by (auto simp:add_ac atLeastLessThanSuc)
    1.16