diff -r 7eb63f63e6c6 -r 279da0358aa9 doc-src/TutorialI/ToyList/document/ToyList.tex --- 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