changeset 66 | 2af87bb52fca |
parent 65 | 633b1fc8631b |
child 67 | 25fd656667a7 |
65:633b1fc8631b | 66:2af87bb52fca |
---|---|
1 theory Correctness |
1 theory Correctness |
2 imports PIPBasics Implementation |
2 imports PIPBasics |
3 begin |
3 begin |
4 |
4 |
5 text {* |
5 text {* |
6 The following two auxiliary lemmas are used to reason about @{term Max}. |
6 The following two auxiliary lemmas are used to reason about @{term Max}. |
7 *} |
7 *} |