# HG changeset patch
# User wenzelm
# Date 1010508201 -3600
# Node ID f85386e8acdf7a9fa657fa87ac4b680e98126df3
# Parent  bb6db6c0d4dff2632e5e31383b702ed06b731dc7
tuned;

diff -r bb6db6c0d4df -r f85386e8acdf doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Tue Jan 08 17:32:40 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy	Tue Jan 08 17:43:21 2002 +0100
@@ -178,12 +178,11 @@
   type declaration given above merely serves for syntactic purposes,
   and is not checked for consistency with the real constant.
 
-  \medskip We may now write either @{text "A [+] B"} or @{text "A \<oplus>
-  B"} in input, while output uses the nicer syntax of $xsymbols$,
-  provided that print mode is active.  Such an arrangement is
-  particularly useful for interactive development, where users may
-  type plain ASCII text, but gain improved visual feedback from the
-  system.
+  \medskip We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in
+  input, while output uses the nicer syntax of $xsymbols$, provided
+  that print mode is active.  Such an arrangement is particularly
+  useful for interactive development, where users may type plain ASCII
+  text, but gain improved visual feedback from the system.
 
   \begin{warn}
   Alternative syntax declarations are apt to result in varying
@@ -360,7 +359,7 @@
   document (\verb,\documentclass, etc.), and to include the generated
   files $T@i$\texttt{.tex} for each theory.  The generated
   \texttt{session.tex} will contain {\LaTeX} commands to include all
-  theory output files in topologically sorted order, so
+  generated files in topologically sorted order, so
   \verb,\input{session}, in \texttt{root.tex} does the job in most
   situations.
 
@@ -412,9 +411,9 @@
   Further packages may be required in particular applications, e.g.\
   for unusual Isabelle symbols.
 
-  \medskip Additional files for the {\LaTeX} stage should be included
-  in the \texttt{MySession/document} directory, e.g.\ further {\TeX}
-  sources or graphics.  In particular, adding \texttt{root.bib} here
+  \medskip Additional files for the {\LaTeX} stage may be included in
+  the directory \texttt{MySession/document}, too, such as {\TeX}
+  sources or graphics).  In particular, adding \texttt{root.bib} here
   (with that specific name) causes an automatic run of \texttt{bibtex}
   to process a bibliographic database; see also \texttt{isatool
   document} covered in \cite{isabelle-sys}.
diff -r bb6db6c0d4df -r f85386e8acdf doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Tue Jan 08 17:32:40 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Tue Jan 08 17:43:21 2002 +0100
@@ -174,11 +174,11 @@
   type declaration given above merely serves for syntactic purposes,
   and is not checked for consistency with the real constant.
 
-  \medskip We may now write either \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while output uses the nicer syntax of $xsymbols$,
-  provided that print mode is active.  Such an arrangement is
-  particularly useful for interactive development, where users may
-  type plain ASCII text, but gain improved visual feedback from the
-  system.
+  \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
+  input, while output uses the nicer syntax of $xsymbols$, provided
+  that print mode is active.  Such an arrangement is particularly
+  useful for interactive development, where users may type plain ASCII
+  text, but gain improved visual feedback from the system.
 
   \begin{warn}
   Alternative syntax declarations are apt to result in varying
@@ -362,7 +362,7 @@
   document (\verb,\documentclass, etc.), and to include the generated
   files $T@i$\texttt{.tex} for each theory.  The generated
   \texttt{session.tex} will contain {\LaTeX} commands to include all
-  theory output files in topologically sorted order, so
+  generated files in topologically sorted order, so
   \verb,\input{session}, in \texttt{root.tex} does the job in most
   situations.
 
@@ -414,9 +414,9 @@
   Further packages may be required in particular applications, e.g.\
   for unusual Isabelle symbols.
 
-  \medskip Additional files for the {\LaTeX} stage should be included
-  in the \texttt{MySession/document} directory, e.g.\ further {\TeX}
-  sources or graphics.  In particular, adding \texttt{root.bib} here
+  \medskip Additional files for the {\LaTeX} stage may be included in
+  the directory \texttt{MySession/document}, too, such as {\TeX}
+  sources or graphics).  In particular, adding \texttt{root.bib} here
   (with that specific name) causes an automatic run of \texttt{bibtex}
   to process a bibliographic database; see also \texttt{isatool
   document} covered in \cite{isabelle-sys}.
diff -r bb6db6c0d4df -r f85386e8acdf doc-src/TutorialI/Makefile
--- a/doc-src/TutorialI/Makefile	Tue Jan 08 17:32:40 2002 +0100
+++ b/doc-src/TutorialI/Makefile	Tue Jan 08 17:43:21 2002 +0100
@@ -48,4 +48,4 @@
 	$(SEDINDEX) $(NAME)
 	$(FIXBOOKMARKS) $(NAME).out
 	$(PDFLATEX) $(NAME)
-	$(FIXBOOKMARKS) main.out
+	$(FIXBOOKMARKS) $(NAME).out