src/HOL/IMP/Hoare_Examples.thy
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)