changeset 32960 | 69916a850301 |
parent 28524 | 644b62cf678f |
child 33639 | 603320b93668 |
32959:23a8c5ac35f8 | 32960:69916a850301 |
---|---|
1 (* Title: HOL/MicroJava/Comp/CorrComp.thy |
1 (* Title: HOL/MicroJava/Comp/CorrComp.thy |
2 ID: $Id$ |
|
3 Author: Martin Strecker |
2 Author: Martin Strecker |
4 *) |
3 *) |
5 |
4 |
6 (* Compiler correctness statement and proof *) |
5 (* Compiler correctness statement and proof *) |
7 |
6 |