1.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 17:29:12 2002 +0100
     1.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 17:29:25 2002 +0100
     1.3 @@ -316,10 +316,10 @@
     1.4  \begin{isamarkuptext}%
     1.5  \noindent The datatype induction rule generated here is of the form
     1.6    \begin{isabelle}%
     1.7 -{\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
     1.8 -\isaindent{\ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
     1.9 -\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
    1.10 -{\isasymLongrightarrow}\ P\ bintree%
    1.11 +\ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
    1.12 +\isaindent{\ \ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
    1.13 +\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
    1.14 +\isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
    1.15  \end{isabelle}%
    1.16  \end{isamarkuptext}%
    1.17  \isamarkuptrue%
    1.18 @@ -748,10 +748,10 @@
    1.19  \isamarkuptrue%
    1.20  %
    1.21  \begin{isamarkuptext}%
    1.22 -By default, Isabelle's document system generates a {\LaTeX} source
    1.23 -  file for each theory that gets loaded while running the session.
    1.24 -  The generated \texttt{session.tex} will include all of these in
    1.25 -  order of appearance, which in turn gets included by the standard
    1.26 +By default, Isabelle's document system generates a {\LaTeX} file for
    1.27 +  each theory that gets loaded while running the session.  The
    1.28 +  generated \texttt{session.tex} will include all of these in order of
    1.29 +  appearance, which in turn gets included by the standard
    1.30    \texttt{root.tex}.  Certainly one may change the order or suppress
    1.31    unwanted theories by ignoring \texttt{session.tex} and load
    1.32    individual files directly in \texttt{root.tex}.  On the other hand,
    1.33 @@ -833,7 +833,8 @@
    1.34    sanity checks here.  Arguments of markup commands and formal
    1.35    comments must not be hidden, otherwise presentation fails.  Open and
    1.36    close parentheses need to be inserted carefully; it is fairly easy
    1.37 -  to hide the wrong parts, especially after rearranging the sources.%
    1.38 +  to hide the wrong parts, especially after rearranging the theory
    1.39 +  text.%
    1.40  \end{isamarkuptext}%
    1.41  \isamarkuptrue%
    1.42  \isamarkupfalse%