diff -r ae84287f44e3 -r a788a05fb81b doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Mon Aug 29 16:18:02 2005 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Aug 29 16:18:03 2005 +0200
@@ -117,26 +117,25 @@
   printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
   output as @{text "A\<^sup>\<star>"}.
 
-  A number of symbols are considered letters by the Isabelle lexer 
-  and can be used as part of identifiers. These are the greek letters
-  @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}, etc apart from
-  @{text "\<lambda>"}, caligraphic letters like @{text "\<A>"}
-  (\verb+\+\verb+<A>+) and @{text "\<AA>"} (\verb+\+\verb+<AA>+), 
-  and the special control symbols \verb+\+\verb+<^isub>+ and 
-  \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This
-  means that the input 
+  A number of symbols are considered letters by the Isabelle lexer and
+  can be used as part of identifiers. These are the greek letters
+  @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}
+  (\verb+\+\verb+<beta>+), etc. (excluding @{text "\<lambda>"}),
+  special letters like @{text "\<A>"} (\verb+\+\verb+<A>+) and @{text
+  "\<AA>"} (\verb+\+\verb+<AA>+), and the control symbols
+  \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
+  sub and super scripts. This means that the input
 
   \medskip
-  {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,}
+  {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
 
   \medskip
   \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"} 
-  by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single entity like 
-  @{text "PA"}, not an exponentiation.
+  by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single
+  syntactic entity, not an exponentiation.
 
-
-  \medskip Replacing our definition of @{text xor} by the following
-  specifies an Isabelle symbol for the new operator:
+  \medskip Replacing our previous definition of @{text xor} by the
+  following specifies an Isabelle symbol for the new operator:
 *}
 
 (*<*)
@@ -380,10 +379,7 @@
   location of the ultimate results.  The above dry run should be able
   to produce some \texttt{document.pdf} (with dummy title, empty table
   of contents etc.).  Any failure at this stage usually indicates
-  technical problems of the {\LaTeX} installation.\footnote{Especially
-  make sure that \texttt{pdflatex} is present; if in doubt one may
-  fall back on DVI output by changing \texttt{usedir} options in
-  \texttt{IsaMakefile} \cite{isabelle-sys}.}
+  technical problems of the {\LaTeX} installation.
 
   \medskip The detailed arrangement of the session sources is as
   follows.
@@ -751,44 +747,47 @@
   no_document use_thy "T";
 \end{verbatim}
 
-  \medskip Theory output may be suppressed more selectively.  Research
-  articles and slides usually do not include the formal content in
-  full.  Delimiting \bfindex{ignored material} by the special source
-  comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
-  preparation system to suppress these parts; the formal checking of
-  the theory is unchanged, of course.
+  \medskip Theory output may be suppressed more selectively, either
+  via \bfindex{tagged command regions} or \bfindex{ignored material}.
 
-  In this example, we hide a theory's \isakeyword{theory} and
-  \isakeyword{end} brackets:
+  Tagged command regions works by annotating commands with named tags,
+  which correspond to certain {\LaTeX} markup that tells how to treat
+  particular parts of a document when doing the actual type-setting.
+  By default, certain Isabelle/Isar commands are implicitly marked up
+  using the predefined tags ``\emph{theory}'' (for theory begin and
+  end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
+  commands involving ML code).  Users may add their own tags using the
+  \verb,%,\emph{tag} notation right after a command name.  In the
+  subsequent example we hide a particularly irrelevant proof:
+*}
 
-  \medskip
+lemma "x = x" by %invisible (simp)
 
-  \begin{tabular}{l}
-  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
-  \texttt{theory T} \\
-  \texttt{imports Main} \\
-  \texttt{begin} \\
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
-  ~~$\vdots$ \\
-  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
-  \texttt{end} \\
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
-  \end{tabular}
+text {*
+  The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
+  Tags observe the structure of proofs; adjacent commands with the
+  same tag are joined into a single region.  The Isabelle document
+  preparation system allows the user to specify how to interpret a
+  tagged region, in order to keep, drop, or fold the corresponding
+  parts of the document.  See the \emph{Isabelle System Manual}
+  \cite{isabelle-sys} for further details, especially on
+  \texttt{isatool usedir} and \texttt{isatool document}.
 
-  \medskip
-
-  Text may be suppressed in a fine-grained manner.  We may even hide
-  vital parts of a proof, pretending that things have been simpler
-  than they really were.  For example, this ``fully automatic'' proof
-  is actually a fake:
+  Ignored material is specified by delimiting the original formal
+  source with special source comments
+  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
+  \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped
+  before the type-setting phase, without affecting the formal checking
+  of the theory, of course.  For example, we may hide parts of a proof
+  that seem unfit for general public inspection.  The following
+  ``fully automatic'' proof is actually a fake:
 *}
 
 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
 
 text {*
-  \noindent Here the real source of the proof has been as follows:
+  \noindent The real source of the proof has been as follows:
 
 \begin{verbatim}
   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
@@ -798,23 +797,7 @@
   \medskip Suppressing portions of printed text demands care.  You
   should not misrepresent the underlying theory development.  It is
   easy to invalidate the visible text by hiding references to
-  questionable axioms.
-
-% 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,),
-  elements need to be kept in mind, too --- the system performs few
-  sanity checks here.  Arguments of markup commands and formal
-  comments must not be hidden, otherwise presentation fails.  Open and
-  close parentheses need to be inserted carefully; it is easy to hide
-  the wrong parts, especially after rearranging the theory text.
+  questionable axioms, for example.
 *}
 
 (*<*)