changeset 89 | 2056d9f481e2 |
parent 88 | 83dd5345d5d0 |
child 90 | ed938e2246b9 |
88:83dd5345d5d0 | 89:2056d9f481e2 |
---|---|
1 <<<<<<< local |
1 theory PrioG |
2 theory Correctness |
2 imports CpsG |
3 imports PIPBasics |
|
4 begin |
3 begin |
5 |
4 |
6 |
5 |
7 text {* |
6 text {* |
8 The following two auxiliary lemmas are used to reason about @{term Max}. |
7 The following two auxiliary lemmas are used to reason about @{term Max}. |
1608 qed |
1607 qed |
1609 |
1608 |
1610 |
1609 |
1611 end |
1610 end |
1612 end |
1611 end |
1613 >>>>>>> other |