author | wenzelm |
Wed, 25 Mar 2015 11:39:52 +0100 | |
changeset 59809 | 87641097d0f3 |
parent 48985 | 5386df44a037 |
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 (*>*)