--- 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