equal
deleted
inserted
replaced
1 (* Title: HOL/Isar_examples/Hoare.thy |
1 (* Title: HOL/Isar_examples/Hoare.thy |
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
4 |
3 |
5 A formulation of Hoare logic suitable for Isar. |
4 A formulation of Hoare logic suitable for Isar. |
6 *) |
5 *) |
7 |
6 |
8 header {* Hoare Logic *} |
7 header {* Hoare Logic *} |
9 |
8 |
10 theory Hoare imports Main |
9 theory Hoare |
11 uses ("~~/src/HOL/Hoare/hoare_tac.ML") begin |
10 imports Main |
|
11 uses ("~~/src/HOL/Hoare/hoare_tac.ML") |
|
12 begin |
12 |
13 |
13 subsection {* Abstract syntax and semantics *} |
14 subsection {* Abstract syntax and semantics *} |
14 |
15 |
15 text {* |
16 text {* |
16 The following abstract syntax and semantics of Hoare Logic over |
17 The following abstract syntax and semantics of Hoare Logic over |