doc-src/TutorialI/Documents/Documents.thy
changeset 15141 a95c2ff210ba
parent 15136 1275417e3930
child 16417 9bc16273c2d4
--- 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$ \\