# HG changeset patch
# User nipkow
# Date 1327044291 -3600
# Node ID ef5d8e94f66f4e3827ca3c544c4e1abc9c90110c
# Parent  0bacd41ce2482a5f7f3e45ad24de3c52b23cd68e
tuned

diff -r 0bacd41ce248 -r ef5d8e94f66f src/HOL/IMP/HoareT.thy
--- a/src/HOL/IMP/HoareT.thy	Fri Jan 20 07:55:43 2012 +0100
+++ b/src/HOL/IMP/HoareT.thy	Fri Jan 20 08:24:51 2012 +0100
@@ -56,7 +56,7 @@
   WHILE Less (V ''y'') (N n)
   DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
 
-lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
+lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
 apply(rule Semi)
 prefer 2
 apply(rule While'