| changeset 15912 | 47aa1a8fcdc9 |
| parent 15561 | 045a07ac35a7 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/HoareParallel/RG_Examples.thy Mon May 02 18:59:50 2005 +0200 +++ b/src/HOL/HoareParallel/RG_Examples.thy Mon May 02 19:00:05 2005 +0200 @@ -154,8 +154,6 @@ subsubsection {* Parameterized *} -declare setsum_op_ivl_Suc [simp] - lemma Example2_lemma2_aux: "j<n \<Longrightarrow> (\<Sum>i=0..<n. (b i::nat)) = (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"