diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Hoare_Examples.thy --- 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)