# HG changeset patch
# User wenzelm
# Date 1383057269 -3600
# Node ID a3c59f04346f066f5ccac6c1c46560a610b61fa8
# Parent  fa80d47c6857abbeb5b55d3ad1e3941895b6c1eb
tuned;

diff -r fa80d47c6857 -r a3c59f04346f src/Doc/IsarRef/Document_Preparation.thy
--- a/src/Doc/IsarRef/Document_Preparation.thy	Wed Oct 16 18:48:37 2013 +0200
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Tue Oct 29 15:34:29 2013 +0100
@@ -5,17 +5,17 @@
 chapter {* Document preparation \label{ch:document-prep} *}
 
 text {* Isabelle/Isar provides a simple document preparation system
-  based on regular {PDF-\LaTeX} technology, with support for
-  hyper-links and bookmarks within that format.  Thus the results are
-  well suited for WWW browsing and as printed copies.
+  based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks
+  within that format.  This allows to produce papers, books, theses
+  etc.\ from Isabelle theory sources.
 
   {\LaTeX} output is generated while processing a \emph{session} in
   batch mode, as explained in the \emph{The Isabelle System Manual}
   \cite{isabelle-sys}.  The main Isabelle tools to get started with
-  document prepation are @{tool_ref mkroot} and @{tool_ref build}.
+  document preparation are @{tool_ref mkroot} and @{tool_ref build}.
 
-  The Isabelle/HOL tutorial \cite{isabelle-hol-book} also covers
-  theory presentation to some extent.  *}
+  The classic Isabelle/HOL tutorial \cite{isabelle-hol-book} also
+  explains some aspects of theory presentation.  *}
 
 
 section {* Markup commands \label{sec:markup} *}
@@ -302,8 +302,8 @@
 subsection {* General options *}
 
 text {* The following options are available to tune the printed output
-  of antiquotations.  Note that many of these coincide with global ML
-  flags of the same names.
+  of antiquotations.  Note that many of these coincide with system and
+  configuration options of the same names.
 
   \begin{description}