
diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Aug 18 11:44:17 2004 +0200
@@ -490,7 +490,7 @@
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
   theory Foo_Bar
-  import Main
+  imports Main
   begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
@@ -767,7 +767,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$ \\




