
diff -r 7eb63f63e6c6 -r 279da0358aa9 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Thu Jul 26 16:43:02 2001 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Jul 26 18:23:38 2001 +0200
@@ -120,7 +120,7 @@
 illustrate not just the basic proof commands but also the typical proof
 process.
 
-\subsubsection*{Main Goal}
+\subsubsection*{Main Goal.}
 
 Our goal is to show that reversing a list twice produces the original
 list.
@@ -140,9 +140,8 @@
 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
 simplification will replace occurrences of @{term"rev(rev xs)"} by
 @{term"xs"}.
-
+\end{itemize}
 The name and the simplification attribute are optional.
-\end{itemize}
 Isabelle's response is to print
 \begin{isabelle}
 proof(prove):~step~0\isanewline




