| changeset 44177 | b4b5cbca2519 |
| parent 43158 | 686fa0a0696e |
| child 44890 | 22f665a2e91c |
--- a/src/HOL/IMP/HoareT.thy Fri Aug 12 20:55:22 2011 -0700 +++ b/src/HOL/IMP/HoareT.thy Sat Aug 13 11:57:13 2011 +0200 @@ -1,6 +1,6 @@ header{* Hoare Logic for Total Correctness *} -theory HoareT imports Hoare_Sound_Complete Util begin +theory HoareT imports Hoare_Sound_Complete begin text{* Now that we have termination, we can define