changeset 15912 | 47aa1a8fcdc9 |
parent 15561 | 045a07ac35a7 |
child 16298 | 8435be7188cb |
--- a/src/HOL/HoareParallel/OG_Examples.thy Mon May 02 18:59:50 2005 +0200 +++ b/src/HOL/HoareParallel/OG_Examples.thy Mon May 02 19:00:05 2005 +0200 @@ -484,8 +484,6 @@ subsubsection {* Increment a Variable in Parallel *} -declare setsum_op_ivl_Suc [simp] - text {* First some lemmas about summation properties. *} (* lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "