1.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Mon Aug 16 19:06:59 2004 +0200
     1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Aug 16 19:47:01 2004 +0200
     1.3 @@ -489,7 +489,9 @@
     1.4    \begin{ttbox}
     1.5    header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
     1.6  
     1.7 -  theory Foo_Bar = Main:
     1.8 +  theory Foo_Bar
     1.9 +  import Main
    1.10 +  begin
    1.11  
    1.12    subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
    1.13  
    1.14 @@ -764,7 +766,9 @@
    1.15  
    1.16    \begin{tabular}{l}
    1.17    \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
    1.18 -  \texttt{theory T = Main:} \\
    1.19 +  \texttt{theory T} \\
    1.20 +  \texttt{import Main} \\
    1.21 +  \texttt{begin} \\
    1.22    \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
    1.23    ~~$\vdots$ \\
    1.24    \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
    1.25 @@ -796,11 +800,13 @@
    1.26    easy to invalidate the visible text by hiding references to
    1.27    questionable axioms.
    1.28  
    1.29 -  Authentic reports of Isabelle/Isar theories, say as part of a
    1.30 -  library, should suppress nothing.  Other users may need the full
    1.31 -  information for their own derivative work.  If a particular
    1.32 -  formalization appears inadequate for general public coverage, it is
    1.33 -  often more appropriate to think of a better way in the first place.
    1.34 +% I removed this because the page overflowed and I disagree a little. TN
    1.35 +%
    1.36 +%  Authentic reports of Isabelle/Isar theories, say as part of a
    1.37 +% library, should suppress nothing.  Other users may need the full
    1.38 +% information for their own derivative work.  If a particular
    1.39 +% formalization appears inadequate for general public coverage, it is
    1.40 +% often more appropriate to think of a better way in the first place.
    1.41  
    1.42    \medskip Some technical subtleties of the
    1.43    \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),