--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jul 26 16:43:02 2001 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jul 26 18:23:38 2001 +0200
@@ -117,7 +117,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.%
@@ -136,9 +136,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 \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
\isa{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