| changeset 63167 | 0909deb8059b |
| parent 62145 | 5b946c81dfbf |
| child 67613 | ce654b0e6d69 |
| 63166:143f58bb34f9 | 63167:0909deb8059b |
|---|---|
1 (* Title: HOL/IMPP/Misc.thy |
1 (* Title: HOL/IMPP/Misc.thy |
2 Author: David von Oheimb, TUM |
2 Author: David von Oheimb, TUM |
3 *) |
3 *) |
4 |
4 |
5 section {* Several examples for Hoare logic *} |
5 section \<open>Several examples for Hoare logic\<close> |
6 |
6 |
7 theory Misc |
7 theory Misc |
8 imports Hoare |
8 imports Hoare |
9 begin |
9 begin |
10 |
10 |