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