diff -r 88ff12baccba -r 0090fab725e3 doc-src/TutorialI/Overview/LNCS/FP0.thy
--- a/doc-src/TutorialI/Overview/LNCS/FP0.thy	Mon Jul 30 16:40:21 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-theory FP0 imports PreList begin
-
-datatype 'a list = Nil                          ("[]")
-                 | Cons 'a "'a list"            (infixr "#" 65)
-
-consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
-       rev :: "'a list \<Rightarrow> 'a list"
-
-primrec
-"[] @ ys       = ys"
-"(x # xs) @ ys = x # (xs @ ys)"
-
-primrec
-"rev []        = []"
-"rev (x # xs)  = (rev xs) @ (x # [])"
-
-theorem rev_rev [simp]: "rev(rev xs) = xs"
-(*<*)oops(*>*)text_raw{*\isanewline\isanewline*}
-
-end