diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 16 19:47:01 2004 +0200
@@ -503,7 +503,9 @@
   \begin{ttbox}
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
-  theory Foo_Bar = Main:
+  theory Foo_Bar
+  import Main
+  begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
 
@@ -793,7 +795,9 @@
 
   \begin{tabular}{l}
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
-  \texttt{theory T = Main:} \\
+  \texttt{theory T} \\
+  \texttt{import Main} \\
+  \texttt{begin} \\
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
   ~~$\vdots$ \\
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
@@ -826,11 +830,13 @@
   easy to invalidate the visible text by hiding references to
   questionable axioms.
 
-  Authentic reports of Isabelle/Isar theories, say as part of a
-  library, should suppress nothing.  Other users may need the full
-  information for their own derivative work.  If a particular
-  formalization appears inadequate for general public coverage, it is
-  often more appropriate to think of a better way in the first place.
+% I removed this because the page overflowed and I disagree a little. TN
+%
+%  Authentic reports of Isabelle/Isar theories, say as part of a
+% library, should suppress nothing.  Other users may need the full
+% information for their own derivative work.  If a particular
+% formalization appears inadequate for general public coverage, it is
+% often more appropriate to think of a better way in the first place.
 
   \medskip Some technical subtleties of the
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),