--- 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