changeset 15136 | 1275417e3930 |
parent 13978 | a241cdd9c1c9 |
child 15141 | a95c2ff210ba |
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 16 19:06:59 2004 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 16 19:47:01 2004 +0200 @@ -1,7 +1,9 @@ % \begin{isabellebody}% \def\isabellecontext{ToyList}% -\isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}\isamarkupfalse% +\isacommand{theory}\ ToyList\isanewline +\isakeyword{import}\ PreList\isanewline +\isakeyword{begin}\isamarkupfalse% % \begin{isamarkuptext}% \noindent