--- 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