--- a/doc-src/Exercises/2000/a1/Snoc.thy Fri Apr 29 18:13:28 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*<*)
-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
-(*>*)