1 header \<open>Using Hoare Logic\<close>
1 section \<open>Using Hoare Logic\<close>
2
3 theory Hoare_Ex
4 imports Hoare
5 begin
6