--- a/doc-src/TutorialI/Overview/LNCS/FP0.thy Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP0.thy Wed Jul 31 17:42:38 2002 +0200
@@ -15,17 +15,6 @@
"rev (x # xs) = (rev xs) @ (x # [])"
theorem rev_rev [simp]: "rev(rev xs) = xs"
-(*<*)oops(*>*)
+(*<*)oops(*>*)text_raw{*\isanewline\isanewline*}
-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