| changeset 41959 | b460124855b8 |
| parent 38353 | d98baa2cf589 |
| child 42054 | 8cd4783904d8 |
| 41958:5abc60a017e0 | 41959:b460124855b8 |
|---|---|
1 (* Title: HOL/Hoare/Hoare.thy |
1 (* Title: HOL/Hoare/Hoare_Logic.thy |
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
3 Copyright 1998 TUM |
3 Copyright 1998 TUM |
4 |
4 |
5 Sugared semantic embedding of Hoare logic. |
5 Sugared semantic embedding of Hoare logic. |
6 Strictly speaking a shallow embedding (as implemented by Norbert Galm |
6 Strictly speaking a shallow embedding (as implemented by Norbert Galm |