equal
deleted
inserted
replaced
1 (* Title: HOL/Hoare/Hoare_Syntax.thy |
1 (* Title: HOL/Hoare/Hoare_Syntax.thy |
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
3 Author: Walter Guttmann (extension to total-correctness proofs) |
3 Author: Walter Guttmann (extension to total-correctness proofs) |
|
4 *) |
4 |
5 |
5 Concrete syntax for Hoare logic, with translations for variables. |
6 section \<open>Concrete syntax for Hoare logic, with translations for variables\<close> |
6 *) |
|
7 |
7 |
8 theory Hoare_Syntax |
8 theory Hoare_Syntax |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |