equal
deleted
inserted
replaced
1 (* Title: HOL/IMP/Hoare.thy |
1 (* Title: HOL/IMP/Hoare.thy |
2 ID: |
2 ID: $$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 |
5 |
6 Semantic embedding of Hoare logic |
6 Semantic embedding of Hoare logic |
7 *) |
7 *) |