# HG changeset patch
# User nipkow
# Date 1115053205 -7200
# Node ID 47aa1a8fcdc9d76fab82fcfad68bcf8de11aa705
# Parent  b730b0edc0853d44062fff39137561d5bc78666d
fixed

diff -r b730b0edc085 -r 47aa1a8fcdc9 src/HOL/HoareParallel/OG_Examples.thy
--- 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 "
diff -r b730b0edc085 -r 47aa1a8fcdc9 src/HOL/HoareParallel/RG_Examples.thy
--- 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))"
diff -r b730b0edc085 -r 47aa1a8fcdc9 src/HOL/Isar_examples/HoareEx.thy
--- 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}.
diff -r b730b0edc085 -r 47aa1a8fcdc9 src/HOL/Isar_examples/Summation.thy
--- 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