summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 16 Jun 2005 11:10:51 +0200 | |

changeset 16409 | a79f8993011b |

parent 16408 | 9bbaa5695691 |

child 16410 | d1a436d92d31 |

*** empty log message ***

--- 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.}