| changeset 9393 | c97111953a66 |
| parent 9034 | ea4dc7603f0b |
| child 9397 | 358e67410253 |
| 9392:c8e6529cc082 | 9393:c97111953a66 |
|---|---|
1 (* Title: hoare_vcg.thy |
1 (* Title: HOL/Hoare/Hoare.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Leonor Prensa Nieto & Tobias Nipkow |
3 Author: Leonor Prensa Nieto & Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 |
5 |
6 Derivation of the proof rules and, most importantly, the VCG tactic. |
6 Derivation of the proof rules and, most importantly, the VCG tactic. |