| changeset 50986 | c54ea7f5418f |
| parent 47818 | 151d137f1095 |
| child 52046 | bc01725d7918 |
--- a/src/HOL/IMP/Hoare_Examples.thy Sat Jan 19 17:42:12 2013 +0100 +++ b/src/HOL/IMP/Hoare_Examples.thy Sat Jan 19 21:05:05 2013 +0100 @@ -5,7 +5,7 @@ subsection{* Example: Sums *} text{* Summing up the first @{text n} natural numbers. The sum is accumulated -in variable @{text 0}, the loop counter is variable @{text 1}. *} +in variable @{text x}, the loop counter is variable @{text y}. *} abbreviation "w n == WHILE Less (V ''y'') (N n)