# HG changeset patch
# User nipkow
# Date 1118424076 -7200
# Node ID 6897b5958be7effcfd24329cd51d41e03b99c2ec
# Parent  af7239e3054d4f98c22c6d8d5dac6616fb0634ac
tuned

diff -r af7239e3054d -r 6897b5958be7 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jun 10 18:36:47 2005 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jun 10 19:21:16 2005 +0200
@@ -117,10 +117,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.}