equal
deleted
inserted
replaced
4 |
4 |
5 header {* Boogie example: get the greatest element of a list *} |
5 header {* Boogie example: get the greatest element of a list *} |
6 |
6 |
7 theory Boogie_Max_Stepwise |
7 theory Boogie_Max_Stepwise |
8 imports Boogie |
8 imports Boogie |
|
9 uses ("Boogie_Max.b2i") |
9 begin |
10 begin |
10 |
11 |
11 text {* |
12 text {* |
12 We prove correct the verification condition generated from the following |
13 We prove correct the verification condition generated from the following |
13 Boogie code: |
14 Boogie code: |