diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{ToyList}% +\isamarkupfalse% % \isadelimtheory % @@ -248,7 +249,6 @@ In order to simplify this subgoal further, a lemma suggests itself.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -304,7 +304,6 @@ embarking on the proof of a lemma usually remains implicit.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -398,7 +397,6 @@ and the missing lemma is associativity of \isa{{\isacharat}}.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}%