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$ \\