equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Hoare_Examples imports Hoare begin |
3 theory Hoare_Examples imports Hoare begin |
|
4 |
|
5 hide_const (open) sum |
4 |
6 |
5 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
7 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
6 |
8 |
7 fun sum :: "int \<Rightarrow> int" where |
9 fun sum :: "int \<Rightarrow> int" where |
8 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |
10 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |