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}%