| changeset 58882 | 6e2010ab8bd9 |
| parent 58614 | 7338eb25226c |
| child 61541 | 846c72206207 |
| 58881:b9556a055632 | 58882:6e2010ab8bd9 |
|---|---|
2 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
3 |
3 |
4 A formulation of Hoare logic suitable for Isar. |
4 A formulation of Hoare logic suitable for Isar. |
5 *) |
5 *) |
6 |
6 |
7 header \<open>Hoare Logic\<close> |
7 section \<open>Hoare Logic\<close> |
8 |
8 |
9 theory Hoare |
9 theory Hoare |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |