doc-src/TutorialI/Documents/document/Documents.tex
changeset 15141 a95c2ff210ba
parent 15136 1275417e3930
child 15481 fc075ae929e4
--- 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$ \\