equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Hoare_Examples imports Hoare Util begin |
3 theory Hoare_Examples imports Hoare begin |
4 |
4 |
5 subsection{* Example: Sums *} |
5 subsection{* Example: Sums *} |
6 |
6 |
7 text{* Summing up the first @{text n} natural numbers. The sum is accumulated |
7 text{* Summing up the first @{text n} natural numbers. The sum is accumulated |
8 in variable @{text 0}, the loop counter is variable @{text 1}. *} |
8 in variable @{text 0}, the loop counter is variable @{text 1}. *} |