# HG changeset patch
# User wenzelm
# Date 1221500590 -7200
# Node ID eee194395fdc865eac821ca99493d56cf9fc03a9
# Parent  402a3f30542f7f8ec8e08b83bf9653e457b9bdac
tuned;

diff -r 402a3f30542f -r eee194395fdc doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Mon Sep 15 19:42:51 2008 +0200
+++ b/doc-src/System/Thy/Basics.thy	Mon Sep 15 19:43:10 2008 +0200
@@ -18,8 +18,9 @@
 
   \begin{itemize}
 
-  \item The \emph{Isabelle settings mechanism} provides environment variables to
-  all Isabelle programs (including tools and user interfaces).
+  \item The \emph{Isabelle settings mechanism} provides environment
+  variables to all Isabelle programs (including tools and user
+  interfaces).
 
   \item The \emph{Isabelle tools wrapper} (@{executable_def isatool})
   provides a generic startup platform for Isabelle related utilities.
@@ -276,7 +277,7 @@
 
 text {*
   All Isabelle related utilities are called via a common wrapper ---
-  \ttindex{isatool}:
+  @{executable isatool}:
 
 \begin{ttbox}
 Usage: isatool TOOL [ARGS ...]
@@ -372,7 +373,7 @@
 *}
 
 
-subsection {* Options *}
+subsubsection {* Options *}
 
 text {*
   If the input heap file does not have write permission bits set, or
@@ -411,8 +412,9 @@
 
   \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
   "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
-  The @{verbatim "-f"} option passes ``@{verbatim "Session.finish ();"}'',
-  which is intended mainly for administrative purposes.
+  The @{verbatim "-f"} option passes ``@{verbatim
+  "Session.finish();"}'', which is intended mainly for administrative
+  purposes.
 
   \medskip The @{verbatim "-m"} option adds identifiers of print modes
   to be made active for this session. Typically, this is used by some
@@ -439,7 +441,7 @@
 *}
 
 
-subsection {* Examples *}
+subsubsection {* Examples *}
 
 text {*
   Run an interactive session of the default object-logic (as specified
@@ -524,4 +526,4 @@
   documentation \cite{proofgeneral} for more information.
 *}
 
-end
+end
\ No newline at end of file