| changeset 64851 | 33aab75ff423 |
| parent 61028 | 99d58362eeeb |
| child 67406 | 23307fd33906 |
--- a/src/HOL/IMP/Hoare_Examples.thy Mon Jan 09 15:54:48 2017 +0000 +++ b/src/HOL/IMP/Hoare_Examples.thy Mon Jan 09 19:32:40 2017 +0100 @@ -2,6 +2,8 @@ theory Hoare_Examples imports Hoare begin +hide_const (open) sum + text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} fun sum :: "int \<Rightarrow> int" where