| changeset 44177 | b4b5cbca2519 |
| parent 43158 | 686fa0a0696e |
| child 44890 | 22f665a2e91c |
--- a/src/HOL/IMP/Hoare_Examples.thy Fri Aug 12 20:55:22 2011 -0700 +++ b/src/HOL/IMP/Hoare_Examples.thy Sat Aug 13 11:57:13 2011 +0200 @@ -1,6 +1,6 @@ (* Author: Tobias Nipkow *) -theory Hoare_Examples imports Hoare Util begin +theory Hoare_Examples imports Hoare begin subsection{* Example: Sums *}