doc-src/TutorialI/ToyList/document/ToyList.tex
changeset 15141 a95c2ff210ba
parent 15136 1275417e3930
child 15364 0c3891c3528f
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 18 11:44:17 2004 +0200
@@ -2,7 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{ToyList}%
 \isacommand{theory}\ ToyList\isanewline
-\isakeyword{import}\ PreList\isanewline
+\isakeyword{imports}\ PreList\isanewline
 \isakeyword{begin}\isamarkupfalse%
 %
 \begin{isamarkuptext}%