doc-src/TutorialI/ToyList/document/ToyList.tex
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