changeset 41589 | bbd861837ebc |
parent 35754 | 8e7dba5f00f5 |
41588:9546828c0eb3 | 41589:bbd861837ebc |
---|---|
1 (* Title: HOL/IMP/Hoare_Op.thy |
1 (* Title: HOL/IMP/Hoare_Op.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
4 *) |
3 *) |
5 |
4 |
6 header "Soundness and Completeness wrt Operational Semantics" |
5 header "Soundness and Completeness wrt Operational Semantics" |
7 |
6 |