*** empty log message ***
authornipkow
Thu, 16 Jun 2005 11:10:51 +0200
changeset 16409 a79f8993011b
parent 16408 9bbaa5695691
child 16410 d1a436d92d31
*** empty log message ***
doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jun 16 10:42:55 2005 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jun 16 11:10:51 2005 +0200
@@ -124,10 +124,10 @@
 \section{An Introductory Proof}
 \label{sec:intro-proof}
 
-Assuming you have input the declarations and definitions of \texttt{ToyList}
-presented so far, we are ready to prove a few simple theorems. This will
-illustrate not just the basic proof commands but also the typical proof
-process.
+Assuming you have processed the declarations and definitions of
+\texttt{ToyList} presented so far, we are ready to prove a few simple
+theorems. This will illustrate not just the basic proof commands but
+also the typical proof process.
 
 \subsubsection*{Main Goal.}