diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/FP0.thy
--- a/doc-src/TutorialI/Overview/FP0.thy	Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-theory FP0 = PreList:
-
-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{*
-\begin{exercise}
-Define a datatype of binary trees and a function @{term mirror}
-that mirrors a binary tree by swapping subtrees recursively. Prove
-@{prop"mirror(mirror t) = t"}.
-
-Define a function @{term flatten} that flattens a tree into a list
-by traversing it in infix order. Prove
-@{prop"flatten(mirror t) = rev(flatten t)"}.
-\end{exercise}
-*}
-end