# HG changeset patch
# User nipkow
# Date 1109838155 -3600
# Node ID 1b3115d1a8df6053092aebc417436c0f1ef36088
# Parent  41bfe19eabe2bb19453b5f7e731c8015c97e063e
fixed proof

diff -r 41bfe19eabe2 -r 1b3115d1a8df src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Thu Mar 03 01:37:32 2005 +0100
+++ b/src/HOL/Isar_examples/HoareEx.thy	Thu Mar 03 09:22:35 2005 +0100
@@ -188,6 +188,8 @@
  state space.
 *}
 
+declare setsum_op_ivl_Suc[simp] atLeast0LessThan[symmetric,simp]
+
 theorem
   "|- .{True}.
       \<acute>S := 0; \<acute>I := 1;