| changeset 65538 | a39ef48fbee0 |
| parent 60304 | 3f429b7d8eb5 |
| child 67613 | ce654b0e6d69 |
| 65537:7ce5fcebfb35 | 65538:a39ef48fbee0 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 (* Compiler correctness statement and proof *) |
5 (* Compiler correctness statement and proof *) |
6 |
6 |
7 theory CorrComp |
7 theory CorrComp |
8 imports "../J/JTypeSafe" "LemmasComp" |
8 imports "../J/JTypeSafe" LemmasComp |
9 begin |
9 begin |
10 |
10 |
11 declare wf_prog_ws_prog [simp add] |
11 declare wf_prog_ws_prog [simp add] |
12 |
12 |
13 (* If no exception is present after evaluation/execution, |
13 (* If no exception is present after evaluation/execution, |