| changeset 16417 | 9bc16273c2d4 |
| parent 13305 | f88d0c363582 |
| child 19249 | 86c73395c99b |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Plus = Main: |
2 theory Plus imports Main begin |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{*\noindent Define the following addition function *} |
5 text{*\noindent Define the following addition function *} |
6 |
6 |
7 consts plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
7 consts plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" |