--- a/doc-src/TutorialI/Overview/FP0.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP0.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -17,7 +17,6 @@
 theorem rev_rev [simp]: "rev(rev xs) = xs"
 (*<*)oops(*>*)
 
-
 text{*
 \begin{exercise}
 Define a datatype of binary trees and a function @{term mirror}
@@ -29,5 +28,4 @@
 @{prop"flatten(mirror t) = rev(flatten t)"}.
 \end{exercise}
 *}
-
 end