# HG changeset patch
# User wenzelm
# Date 1011025765 -3600
# Node ID c0ce43e809fd26772716bd5a924e59ddba5eb8a7
# Parent  4cc93529646d275eb6aa653a5b5e1e5ffbb7a366
updated;

diff -r 4cc93529646d -r c0ce43e809fd doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 17:29:12 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 17:29:25 2002 +0100
@@ -316,10 +316,10 @@
 \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%
+\ {\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
+\isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
 \end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -748,10 +748,10 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-By default, Isabelle's document system generates a {\LaTeX} source
-  file for each theory that gets loaded while running the session.
-  The generated \texttt{session.tex} will include all of these in
-  order of appearance, which in turn gets included by the standard
+By default, Isabelle's document system generates a {\LaTeX} file for
+  each theory that gets loaded while running the session.  The
+  generated \texttt{session.tex} will include all of these in order of
+  appearance, which in turn gets included by the standard
   \texttt{root.tex}.  Certainly one may change the order or suppress
   unwanted theories by ignoring \texttt{session.tex} and load
   individual files directly in \texttt{root.tex}.  On the other hand,
@@ -833,7 +833,8 @@
   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 fairly easy
-  to hide the wrong parts, especially after rearranging the sources.%
+  to hide the wrong parts, especially after rearranging the theory
+  text.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%