author | haftmann |
Tue, 09 Aug 2005 08:56:34 +0200 | |
changeset 17036 | 9b57e5aa4c93 |
parent 16417 | 9bc16273c2d4 |
child 19249 | 86c73395c99b |
permissions | -rw-r--r-- |
(*<*) theory Plus imports Main begin (*>*) text{*\noindent Define the following addition function *} consts plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" primrec "plus m 0 = m" "plus m (Suc n) = plus (Suc m) n" text{*\noindent and prove*} (*<*) lemma [simp]: "!m. plus m n = m+n" apply(induct_tac n) by(auto) (*>*) lemma "plus m n = m+n" (*<*) by(simp) end (*>*)