tuned
authornipkow
Fri, 20 Jan 2012 08:24:51 +0100
changeset 46304 ef5d8e94f66f
parent 46303 0bacd41ce248
child 46305 8ea02e499d53
tuned
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'