--- 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 "
--- 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))"
--- a/src/HOL/Isar_examples/HoareEx.thy Mon May 02 18:59:50 2005 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy Mon May 02 19:00:05 2005 +0200
@@ -188,7 +188,7 @@
state space.
*}
-declare setsum_op_ivl_Suc[simp] atLeast0LessThan[symmetric,simp]
+declare atLeast0LessThan[symmetric,simp]
theorem
"|- .{True}.
--- a/src/HOL/Isar_examples/Summation.thy Mon May 02 18:59:50 2005 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Mon May 02 19:00:05 2005 +0200
@@ -9,8 +9,6 @@
imports Main
begin
-declare setsum_op_ivl_Suc [simp] setsum_cl_ivl_Suc [simp]
-
text_raw {*
\footnote{This example is somewhat reminiscent of the
\url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is