diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Overview/LNCS/FP0.thy
--- 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