| changeset 41589 | bbd861837ebc |
| parent 28524 | 644b62cf678f |
| child 58889 | 5b7a9633cfa8 |
| 41588:9546828c0eb3 | 41589:bbd861837ebc |
|---|---|
1 (* Title: HOL/IMPP/Misc.thy |
1 (* Title: HOL/IMPP/Misc.thy |
2 ID: $Id$ |
2 Author: David von Oheimb, TUM |
3 Author: David von Oheimb |
|
4 Copyright 1999 TUM |
|
5 *) |
3 *) |
6 |
4 |
7 header {* Several examples for Hoare logic *} |
5 header {* Several examples for Hoare logic *} |
8 |
6 |
9 theory Misc |
7 theory Misc |