author | kleing |
Mon, 29 Dec 2003 06:49:26 +0100 | |
changeset 14333 | 14f29eb097a3 |
parent 13739 | f5d0a66c8124 |
permissions | -rw-r--r-- |
(*<*) theory Snoc = Main: (*>*) subsection {* Lists *} text {* Define a primitive recursive function @{text snoc} that appends an element at the \emph{right} end of a list. Do not use @{text"@"} itself. *} consts snoc :: "'a list => 'a => 'a list" text {* Prove the following theorem: *} theorem rev_cons: "rev (x # xs) = snoc (rev xs) x" (*<*)oops(*>*) text {* Hint: you need to prove a suitable lemma first. *} (*<*) end (*>*)