equal
deleted
inserted
replaced
5 A formulation of Hoare logic suitable for Isar. |
5 A formulation of Hoare logic suitable for Isar. |
6 *) |
6 *) |
7 |
7 |
8 header {* Hoare Logic *} |
8 header {* Hoare Logic *} |
9 |
9 |
10 theory Hoare = Main |
10 theory Hoare imports Main |
11 files ("~~/src/HOL/Hoare/hoare.ML"): |
11 uses ("~~/src/HOL/Hoare/hoare.ML") begin |
12 |
12 |
13 subsection {* Abstract syntax and semantics *} |
13 subsection {* Abstract syntax and semantics *} |
14 |
14 |
15 text {* |
15 text {* |
16 The following abstract syntax and semantics of Hoare Logic over |
16 The following abstract syntax and semantics of Hoare Logic over |