# 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 "\\<^sub>t {\s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\s. s ''x'' = \ {1 .. n}}" +lemma "\\<^sub>t {\s. 0 \ n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\s. s ''x'' = \{1..n}}" apply(rule Semi) prefer 2 apply(rule While'