author | wenzelm |
Mon, 09 Mar 2009 11:57:48 +0100 | |
changeset 30382 | 910290f04692 |
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 (*>*)