author | wenzelm |
Tue, 28 Aug 2012 18:57:32 +0200 | |
changeset 48985 | 5386df44a037 |
parent 27015 | doc-src/TutorialI/Misc/Plus.thy@f8537d69f514 |
child 67406 | 23307fd33906 |
permissions | -rw-r--r-- |
(*<*) theory Plus imports Main begin (*>*) text{*\noindent Define the following addition function *} primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where "add m 0 = m" | "add m (Suc n) = add (Suc m) n" text{*\noindent and prove*} (*<*) lemma [simp]: "!m. add m n = m+n" apply(induct_tac n) by(auto) (*>*) lemma "add m n = m+n" (*<*) by(simp) end (*>*)