diff -r 8e1b3d425b71 -r d7b4d8c9bf86 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 16:09:25 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 16:09:29 2002 +0100
@@ -297,7 +297,52 @@
   proofs formally, the theory sources are turned into typesetting
   instructions in a schematic manner.  This enables users to write
   authentic reports on theory developments with little effort, where
-  most consistency checks are handled by the system.%
+  most consistency checks are handled by the system.
+
+  Here is an example to illustrate the idea of Isabelle document
+  preparation.
+
+  \bigskip The following datatype definition of \isa{{\isacharprime}a\ bintree}
+  models binary trees with nodes being decorated by elements of type
+  \isa{{\isacharprime}a}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
+\ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent The datatype induction rule generated here is of the form
+  \begin{isabelle}%
+{\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
+\isaindent{\ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
+\isaindent{\ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
+{\isasymLongrightarrow}\ P\ bintree%
+\end{isabelle}
+
+  \bigskip The above document output has been produced by the
+  following theory specification:
+
+  \begin{ttbox}
+  text {\ttlbrace}*
+    The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
+    models binary trees with nodes being decorated by elements
+    of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
+  *{\ttrbrace}
+
+  datatype 'a bintree =
+    Leaf | Branch 'a  "'a bintree"  "'a bintree"
+
+  text {\ttlbrace}*
+    {\ttback}noindent The datatype induction rule generated here is
+    of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
+  *{\ttrbrace}
+  \end{ttbox}
+
+  Here we have augmented the theory by formal comments (via
+  \isakeyword{text} blocks).  The informal parts may again refer to
+  formal entities by means of ``antiquotations'' (such as
+  \texttt{\at}\verb,{text "'a bintree"}, or
+  \texttt{\at}\verb,{typ 'a},; see also \S\ref{sec:doc-prep-text}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -337,7 +382,8 @@
   \texttt{IsaMakefile} \cite{isabelle-sys}.}
 
   \medskip The detailed arrangement of the session sources is as
-  follows; advanced
+  follows.  This may be ignored in the beginning, but some of these
+  files need to be edited in realistic applications.
 
   \begin{itemize}
 
@@ -473,10 +519,10 @@
   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
 \end{verbatim}
 
-  \noindent That particular modification requires to change the
-  default \verb,\documentclass{article}, in \texttt{root.tex} to
-  something that supports the notion of chapters in the first place,
-  such as \verb,\documentclass{report},.
+  \noindent That particular modification requires change to the
+  document class given in \texttt{root.tex} to something that supports
+  the notion of chapters in the first place, such as
+  \verb,\documentclass{report},.
 
   \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
   hold the name of the current theory context.  This is particularly
@@ -493,12 +539,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Formal Comments and Antiquotations%
+\isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Isabelle source comments, which are of the form
+Isabelle \bfindex{source comments}, which are of the form
   \verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white
   space and do not really contribute to the content.  They mainly
   serve technical purposes to mark certain oddities in the raw input