
diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Aug 18 11:44:17 2004 +0200
@@ -504,7 +504,7 @@
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
   theory Foo_Bar
-  import Main
+  imports Main
   begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
@@ -796,7 +796,7 @@
   \begin{tabular}{l}
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
   \texttt{theory T} \\
-  \texttt{import Main} \\
+  \texttt{imports Main} \\
   \texttt{begin} \\
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
   ~~$\vdots$ \\




