author | wenzelm |
Sat, 11 Mar 2006 17:30:35 +0100 | |
changeset 19249 | 86c73395c99b |
parent 16417 | 9bc16273c2d4 |
child 27015 | f8537d69f514 |
permissions | -rw-r--r-- |
(*<*) theory Plus imports Main begin (*>*) text{*\noindent Define the following addition function *} consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat" primrec "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 (*>*)