author | immler@in.tum.de |
Thu, 26 Feb 2009 10:13:43 +0100 | |
changeset 30151 | 629f3a92863e |
parent 27015 | f8537d69f514 |
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 (*>*)