1 section {* Addition with fixpoint of successor *}
1 section \<open>Addition with fixpoint of successor\<close>
2
3 theory Ex3
4 imports "../LCF"
5 begin
6