--- 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;