| changeset 38432 | 439f50a241c1 |
| parent 38430 | 254a021ed66e |
| child 48966 | 6e15de7dd871 |
--- a/doc-src/TutorialI/ToyList/ToyList.thy Sun Aug 15 16:48:58 2010 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Sun Aug 15 17:14:10 2010 +0200 @@ -124,7 +124,8 @@ value "rev (a # b # c # [])" -text{* +text{*\noindent yields @{term"c # b # a # []"}. + \section{An Introductory Proof} \label{sec:intro-proof}