diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/Overview/FP0.thy
--- a/doc-src/TutorialI/Overview/FP0.thy	Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP0.thy	Fri Jun 21 18:40:06 2002 +0200
@@ -1,7 +1,5 @@
 theory FP0 = PreList:
 
-section{*Functional Programming/Modelling*}
-
 datatype 'a list = Nil                          ("[]")
                  | Cons 'a "'a list"            (infixr "#" 65)
 
@@ -16,10 +14,8 @@
 "rev []        = []"
 "rev (x # xs)  = (rev xs) @ (x # [])"
 
-subsection{*An Introductory Proof*}
-
 theorem rev_rev [simp]: "rev(rev xs) = xs"
-oops
+(*<*)oops(*>*)
 
 
 text{*