1 header {* Addition with fixpoint of successor *}
1 section {* Addition with fixpoint of successor *}
2
3 theory Ex3
4 imports LCF
5 begin
6