--- a/doc-src/System/present.tex Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/present.tex Tue Dec 11 15:36:28 2001 +0100
@@ -6,21 +6,40 @@
Isabelle provides several ways to present the outcome of formal developments,
including WWW-based browsable libraries or actual printable documents.
Presentation is centered around the concept of \emph{logic sessions}. The
-global session structure is that of a tree, with Isabelle \texttt{Pure} at its
-root, further object-logics derived (e.g.\ \texttt{HOLCF} from \texttt{HOL},
-and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf
-positions. The latter usually do not have a separate {\ML} image.
+global session structure is that of a tree, with Isabelle Pure at its root,
+further object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
+application sessions in leaf positions (usually without a separate image).
The \texttt{mkdir} (see \S\ref{sec:tool-mkdir}) and \texttt{make} (see
\S\ref{sec:tool-make}) tools of Isabelle provide the primary means for
managing Isabelle sessions, including proper setup for presentation. Here the
-\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to run any
-additional stages required for document preparation, notably the tools
-\texttt{document} (see \S\ref{sec:tool-document}) and \texttt{latex} (see
-\S\ref{sec:tool-latex}).
+\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to let the
+\texttt{isabelle} process run any additional stages required for document
+preparation, notably the tools \texttt{document} (see
+\S\ref{sec:tool-document}) and \texttt{latex} (see \S\ref{sec:tool-latex}).
+The complete tool chain for managing batch-mode Isabelle sessions is
+illustrated in figure~\ref{fig:session-tools}.
+
+\begin{figure}[htbp]
+ \begin{center}
+ \begin{tabular}{lp{0.6\textwidth}}
+ \texttt{isatool mkdir} & invoked once by the user to create the initial
+ source setup (common \texttt{IsaMakefile} plus a single session directory); \\
+ \texttt{isatool make} & invoked repeatedly by the user to
+ keep session output up-to-date (HTML, documents etc.); \\
+ \texttt{isatool usedir} & part of the standard \texttt{IsaMakefile} entry of a session; \\
+ \texttt{isabelle} & run through \texttt{isatool usedir}; \\
+ \texttt{isatool document} & run by the Isabelle process if document preparation is enabled; \\
+ \texttt{isatool latex} & universal {\LaTeX} tool wrapper invoked multiple times
+ by \texttt{isatool document}; also useful for manual experiments; \\
+ \end{tabular}
+ \caption{The tool chain of Isabelle session presentation}
+ \label{fig:session-tools}
+ \end{center}
+\end{figure}
-\section{Generating theory browsing information} \label{sec:info}
+\section{Generating theory browser information} \label{sec:info}
\index{theory browsing information|bold}
As a side-effect of running a logic sessions, Isabelle is able to generate
@@ -34,36 +53,44 @@
Isabelle also generates graph files that represent the theory hierarchy of a
logic. There is a graph browser Java applet embedded in the generated HTML
pages, and also a stand-alone application that allows browsing theory graphs
-without having to start a WWW browser first. The latter version also includes
+without having to start a WWW client first. The latter version also includes
features such as generating Postscript files, which are not available in the
applet version. See \S\ref{sec:browse} for further information.
\medskip
-In order to let Isabelle generate theory browsing information, simply append
-``\texttt{-i true}'' to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before
-making a logic. For example, in order to do this for FOL, add this to your
-Isabelle settings file
+The easiest way to let Isabelle generate theory browsing information for
+existing sessions is to append ``\texttt{-i true}'' to the
+\settdx{ISABELLE_USEDIR_OPTIONS} before invoking \texttt{isatool make} (or
+\texttt{./build} in the distribution). For example, add something like this
+to your Isabelle settings file
\begin{ttbox}
ISABELLE_USEDIR_OPTIONS="-i true"
\end{ttbox}
and then change into the \texttt{src/FOL} directory of the Isabelle
distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
+The presentation output will appear in \texttt{\$ISABELLE_BROWSER_INFO/FOL},
+which usually refers to \verb,~/isabelle/browser_info/FOL,. Note that option
+\texttt{-v true} will make the internal runs of \texttt{usedir} more explicit
+about such details.
-Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual
+Many standard Isabelle sessions (such as \texttt{HOL/ex}) also provide actual
printable documents. These are prepared automatically as well if enabled like
this, using the \texttt{-d} option
\begin{ttbox}
ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
\end{ttbox}
-See \S\ref{sec:tool-document} for further information on Isabelle document
-preparation.
+Enabling options \texttt{-i} and \texttt{-d} simultaneausly as shown above
+causes an appropriate ``document'' link to be included in the HTML index.
+Documents (or raw document sources) may be generated independently of browser
+information as well, see \S\ref{sec:tool-document} for further details.
-\bigskip The theory browsing information is stored within the directory
-determined by the \settdx{ISABELLE_BROWSER_INFO} setting. The
-\texttt{index.html} file located there provides an entry point to all standard
-Isabelle logics. A complete HTML version of all object-logics and examples of
-the Isabelle distribution is available at
+\bigskip The theory browsing information is stored in a sub-directory
+directory determined by the \settdx{ISABELLE_BROWSER_INFO} setting plus a
+prefix corresponding to the session identifier (according to the tree
+structure of sub-sessions by default). A complete WWW view of all standard
+object-logics and examples of the Isabelle distribution is available at the
+Cambridge or Munich Isabelle sites:
\begin{center}\small
\begin{tabular}{l}
\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
@@ -71,31 +98,19 @@
\end{tabular}
\end{center}
-\medskip
-
-The generated HTML document of any theory includes all theorems proved in the
-corresponding {\ML} file, provided these have been stored properly via
-\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm},
-\ttindex{bind_thms} or \ttindex{store_thm} (see also \cite{isabelle-ref}).
-Section headings may be included in the presentation via the {\ML} function
-\begin{ttbox}\index{*section}
-section: string -> unit
-\end{ttbox}
-
-\medskip
-
-In order to present your own theories on the web, simply copy the
+\medskip In order to present your own theories on the web, simply copy the
corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW
-server, after having generated browser info like this:
+server, having generated browser info like this:
\begin{ttbox}
isatool usedir -i true HOL Foo
\end{ttbox}
This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
-to load all your theories, and HOL is your parent logic image. Ideally,
-theory browser information would have been generated for HOL already.
-
-Alternatively, one may specify an external link to an existing body of HTML
-data by giving \texttt{usedir} a \texttt{-P} option like this:
+to load all your theories, and HOL is your parent logic image (\texttt{isatool
+ mkdir} assists in setting up Isabelle session directories, see
+\S\ref{sec:tool-mkdir}). Theory browser information for HOL should have been
+generated already beforehand. Alternatively, one may specify an external link
+to an existing body of HTML data by giving \texttt{usedir} a \texttt{-P}
+option like this:
\begin{ttbox}
isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
\end{ttbox}
@@ -105,8 +120,7 @@
There is a separate \texttt{mkdir} tool to provide easy setup of all this,
with only minimal manual editing required.
\begin{ttbox}
-isatool mkdir Foo
-isatool make
+isatool mkdir HOL Foo && isatool make
\end{ttbox}
See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session
directories, including the setup for documents.
@@ -115,11 +129,14 @@
\section{Browsing theory graphs} \label{sec:browse}
\index{theory graph browser|bold}
-The graph browser is a tool for visualizing dependency graphs. Certain nodes
-of the graph (i.e.~theories) can be grouped together in ``directories'', whose
-contents may be hidden, thus enabling the user to filter out irrelevant
-information. The browser is written in Java, it can be used both as a
-stand-alone application and as an applet.
+The Isabelle graph browser is a general tool for visualizing dependency
+graphs. Certain nodes of the graph (i.e.~theories) can be grouped together in
+``directories'', whose contents may be hidden, thus enabling the user to
+collapse irrelevant portions of information. The browser is written in Java,
+it can be used both as a stand-alone application and as an applet. Note that
+the option \texttt{-g} of \texttt{isatool usedir} (see
+\S\ref{sec:tool-usedir}) creates graph presentations in batch mode for
+inclusion in session documents.
\subsection{Invoking the graph browser}
@@ -145,12 +162,12 @@
\subsection{Using the graph browser}
The browser's main window, which is shown in figure
-\ref{browserwindow}, consists of two sub-windows: In the left
+\ref{fig:browserwindow}, consists of two sub-windows: In the left
sub-window, the directory tree is displayed. The graph itself is
displayed in the right sub-window.
\begin{figure}[ht]
\includegraphics[width=\textwidth]{browser_screenshot}
- \caption{\label{browserwindow} Browser main window}
+ \caption{\label{fig:browserwindow} Browser main window}
\end{figure}
@@ -205,7 +222,7 @@
\item[Open \dots] Open a new graph file.
\item[Export to PostScript] Outputs the current graph in Postscript format,
- appropriately scaled to fit on one single sheet of paper. The resulting
+ appropriately scaled to fit on one single sheet of A4 paper. The resulting
file can be printed directly.
\item[Export to EPS] Outputs the current graph in Encapsulated Postscript
@@ -250,115 +267,6 @@
\end{description}
-\section{Preparing Isabelle session documents --- \texttt{isatool document}}
-\label{sec:tool-document}
-
-The \tooldx{document} utility prepares logic session documents, processing the
-sources both as provided by the user and generated by Isabelle. Its usage is:
-\begin{ttbox}
-Usage: document [OPTIONS] [DIR]
-
- Options are:
- -c cleanup -- be aggressive in removing old stuff
- -o FORMAT specify output format: dvi (default), dvi.gz, ps,
- ps.gz, pdf
- -v be verbose
-
- Prepare the theory session document in DIR (default 'document')
- producing the specified output format.
-\end{ttbox}
-This tool is usually run automatically as part of the corresponding session,
-provided document preparation has been enabled (cf.\ the \texttt{-d} option of
-the \texttt{usedir} utility, \S\ref{sec:tool-usedir}). It may be manually
-invoked on the generated browser information document output as well.
-
-\medskip Document preparation requires a properly setup ``\texttt{document}''
-directory within the logic session sources. This directory is supposed to
-contain all the files needed to produce the final document --- apart from the
-actual theories which are generated by Isabelle.
-
-\medskip For simple documents, the \texttt{document} tool is smart enough to
-create any of the output formats, taking \texttt{root.tex} supplied by the
-user as a starting point. This even includes multiple runs of {\LaTeX} to
-accommodate references and bibliographies (the latter assumes
-\texttt{root.bib} within the same directory).
-
-For complex documents, a separate \texttt{IsaMakefile} may be given instead.
-It should provide targets for any admissible document format; these have to
-produce corresponding output files named after \texttt{root} as well, e.g.\
-\texttt{root.dvi} for target format \texttt{dvi}.
-
-\medskip When running the session, Isabelle copies the original
-\texttt{document} directory into its proper place within
-\texttt{ISABELLE_BROWSER_INFO} according to the session path. Then, for any
-processed theory $A$ some {\LaTeX} source is generated and put there as
-$A$\texttt{.tex}. Furthermore, a list of all generated theory files is put
-into \texttt{session.tex}. Typically, the root {\LaTeX} file provided by the
-user would include \texttt{session.tex} to get a document containing all the
-theories.
-
-The {\LaTeX} versions of the theories require some macros defined in
-\texttt{isabelle.sty} as distributed with Isabelle. Doing
-\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
-the underlying Isabelle \texttt{latex} utility already includes an appropriate
-{\TeX} inputs path.
-
-If the text contains any references to Isabelle symbols (such as
-\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
-This package contains a standard set of {\LaTeX} macro definitions
-\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
-Appendix~\ref{app:symbols} for a complete list). The user may refer to
-further symbols as well, simply by providing {\LaTeX} macros of the same sort.
-
-For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
-images), we recommend to include \verb,pdfsetup.sty, as well. It is safe to
-do so even without using PDF~\LaTeX.
-
-\medskip As a final step, \texttt{isatool document -c} is run on the resulting
-\texttt{document} directory. Thus the actual output document is built and
-installed in its proper place (as linked by the session's
-\texttt{index.html}). The generated sources are deleted after successful run
-of {\LaTeX} and friends. Note that a copy of the sources may be retained by
-passing an option \texttt{-D} to the \texttt{usedir} utility when running the
-session (see also \S\ref{sec:tool-usedir}).
-
-
-\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
-\label{sec:tool-latex}
-
-The \tooldx{latex} utility provides the basic interface for Isabelle document
-preparation. Its usage is:
-\begin{ttbox}
-Usage: latex [OPTIONS] [FILE]
-
- Options are:
- -o FORMAT specify output format: dvi (default), dvi.gz, ps,
- ps.gz, pdf, bbl, png, sty
-
- Run LaTeX (and related tools) on FILE (default root.tex),
- producing the specified output format.
-\end{ttbox}
-Appropriate {\LaTeX}-related programs are run on the input file, according to
-the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
-\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
-The actual commands are determined from the settings environment
-(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
-
-The \texttt{sty} output format causes the Isabelle style files to be updated
-from the distribution. This is useful in special situations where the
-document sources are to be processed another time by separate tools (cf.\
-option \texttt{-D} of the \texttt{usedir} utility, see
-\S\ref{sec:tool-usedir}).
-
-It is important to note that the {\LaTeX} inputs file space has to be properly
-setup to include the Isabelle styles. Usually, this may be done by modifying
-the \settdx{TEXINPUTS} variable in settings like this:
-\begin{ttbox}
-TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
-\end{ttbox}
-This is known to work with recent versions of the \textsl{teTeX} distribution.
-
-
\section{Creating Isabelle session directories --- \texttt{isatool mkdir}}
\label{sec:tool-mkdir}
@@ -367,7 +275,7 @@
and a \texttt{document} directory with a minimal \texttt{root.tex} that is
sufficient print all theories of the session (in the order of appearance); see
\S\ref{sec:tool-document} for further information on Isabelle document
-preparation. The usage of \texttt{mkdir} is:
+preparation. The usage of \texttt{isatool mkdir} is:
\begin{ttbox}
Usage: mkdir [OPTIONS] [LOGIC] NAME
@@ -383,7 +291,7 @@
The \texttt{mkdir} tool is conservative in the sense that any existing
\texttt{IsaMakefile} etc.\ is left unchanged. Thus it is safe to invoke it
-experimentally, with varying options.
+multiple times, although later runs may not have the desired effect.
Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile}
incrementally --- manual changes are required for multiple sub-sessions. On
@@ -420,16 +328,23 @@
The standard setup of a single ``example session'' based on the default logic,
with proper document generation is generated like this:
\begin{ttbox}
-isatool mkdir Foo
-isatool make
+isatool mkdir Foo && isatool make
\end{ttbox}
\noindent The theory sources should be put into the \texttt{Foo} directory, and its
\texttt{ROOT.ML} should be edited to load all required theories. Invoking
-\texttt{isatool make} would now run the whole session, generating browser
+\texttt{isatool make} again would run the whole session, generating browser
information and the document automatically. The \texttt{IsaMakefile} is
-usually tuned manually later, e.g.\ adding actual source dependencies, or
+typically tuned manually later, e.g.\ adding actual source dependencies, or
changing the options passed to \texttt{usedir}.
+\medskip Large projects may demand further sessions, potentially with separate
+logic images being created. This usually requires manual editing of the
+generated \texttt{IsaMakefile}, which is meant to cover all of the sub-session
+directories at the same time (this is the deeper reasong why
+\texttt{IsaMakefile} is not made part of the initial session directory created
+by \texttt{isatool mkdir}). See \texttt{src/HOL/IsaMakefile} of the Isabelle
+distribution for a full-blown example.
+
\section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
@@ -445,6 +360,7 @@
-b build mode (output heap image, using current dir)
-c BOOL tell ML system to compress output image (default true)
-d FORMAT build document as FORMAT (default false)
+ -g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
-p LEVEL set level of detail for proof objects
@@ -500,6 +416,14 @@
\texttt{document} directory. See \S\ref{sec:tool-document} and
\S\ref{sec:tool-latex} for more details.
+The \texttt{-g} option produces images of the theory dependency graph (cf.\
+\S\ref{sec:browse}) for inclusion in the generated document, both as
+\texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
+In order to make this appear the final {\LaTeX} document one would typically
+say \verb,\includegraphics{session_graph}, in the \texttt{document/root.tex}
+file. (Omitting the file-name extension enables {\LaTeX} to select to correct
+version, either for the DVI or PDF output path.)
+
\medskip The \texttt{-D} option causes the generated document sources to be
dumped at location \texttt{PATH}, which is relative to the session's main
directory. For example, \texttt{-D document} would leave a copy of the
@@ -533,6 +457,135 @@
\S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation
of \texttt{usedir} as well.
+
+\section{Preparing Isabelle session documents --- \texttt{isatool document}}
+\label{sec:tool-document}
+
+The \tooldx{document} utility prepares logic session documents, processing the
+sources both as provided by the user and generated by Isabelle. Its usage is:
+\begin{ttbox}
+Usage: document [OPTIONS] [DIR]
+
+ Options are:
+ -c cleanup -- be aggressive in removing old stuff
+ -o FORMAT specify output format: dvi (default), dvi.gz, ps,
+ ps.gz, pdf
+
+ Prepare the theory session document in DIR (default 'document')
+ producing the specified output format.
+\end{ttbox}
+This tool is usually run automatically as part of the corresponding Isabelle
+batch process, provided document preparation has been enabled (cf.\ the
+\texttt{-d} option of the \texttt{usedir} utility, \S\ref{sec:tool-usedir}).
+It may be manually invoked on the generated browser information document
+output as well, e.g.\ in case of errors encountered in the batch run.
+
+\medskip Document preparation requires a properly setup ``\texttt{document}''
+directory within the logic session sources. This directory is supposed to
+contain all the files needed to produce the final document --- apart from the
+actual theories which are generated by Isabelle.
+
+\medskip For most practical purposes, the \texttt{document} tool is smart
+enough to create any of the specified output formats, taking \texttt{root.tex}
+supplied by the user as a starting point. This even includes multiple runs of
+{\LaTeX} to accommodate references and bibliographies (the latter assumes
+\texttt{root.bib} within the same directory).
+
+In more complex situations, a separate \texttt{IsaMakefile} for the document
+sources may be given instead. This should provide targets for any admissible
+document format; these have to produce corresponding output files named after
+\texttt{root} as well, e.g.\ \texttt{root.dvi} for target format \texttt{dvi}.
+
+\medskip When running the session, Isabelle copies the original
+\texttt{document} directory into its proper place within
+\texttt{ISABELLE_BROWSER_INFO} according to the session path. Then, for any
+processed theory $A$ some {\LaTeX} source is generated and put there as
+$A$\texttt{.tex}. Furthermore, a list of all generated theory files is put
+into \texttt{session.tex}. Typically, the root {\LaTeX} file provided by the
+user would include \texttt{session.tex} to get a document containing all the
+theories.
+
+The {\LaTeX} versions of the theories require some macros defined in
+\texttt{isabelle.sty} as distributed with Isabelle. Doing
+\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
+the underlying Isabelle \texttt{latex} utility already includes an appropriate
+{\TeX} inputs path.
+
+If the text contains any references to Isabelle symbols (such as
+\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
+This package contains a standard set of {\LaTeX} macro definitions
+\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
+Appendix~\ref{app:symbols} for a complete list of predefined Isabelle
+symbols). Users may invent further symbols as well, just by providing
+{\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the
+distribution.
+
+For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
+images), we recommend to include \verb,pdfsetup.sty, as well. It is safe to
+do so even without using PDF~\LaTeX.
+
+\medskip As a final step of document preparation within Isabelle,
+\texttt{isatool document -c} is run on the resulting \texttt{document}
+directory. Thus the actual output document is built and installed in its
+proper place (as linked by the session's \texttt{index.html} if option
+\texttt{-i} of \texttt{usedir} has been enabled, cf.\ \S\ref{sec:info}). The
+generated sources are deleted after successful run of {\LaTeX} and friends.
+Note that a separate copy of the sources may be retained by passing an option
+\texttt{-D} to the \texttt{usedir} utility when running the session (see also
+\S\ref{sec:tool-usedir}).
+
+
+\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
+\label{sec:tool-latex}
+
+The \tooldx{latex} utility provides the basic interface for Isabelle document
+preparation. Its usage is:
+\begin{ttbox}
+Usage: latex [OPTIONS] [FILE]
+
+ Options are:
+ -o FORMAT specify output format: dvi (default), dvi.gz, ps,
+ ps.gz, pdf, bbl, png, sty
+
+ Run LaTeX (and related tools) on FILE (default root.tex),
+ producing the specified output format.
+\end{ttbox}
+Appropriate {\LaTeX}-related programs are run on the input file, according to
+the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
+\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
+The actual commands are determined from the settings environment
+(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
+
+The \texttt{sty} output format causes the Isabelle style files to be updated
+from the distribution. This is useful in special situations where the
+document sources are to be processed another time by separate tools (cf.\
+option \texttt{-D} of the \texttt{usedir} utility, see
+\S\ref{sec:tool-usedir}).
+
+It is important to note that the {\LaTeX} inputs file space has to be properly
+setup to include the Isabelle styles. Usually, this may be done by modifying
+the \settdx{TEXINPUTS} variable in the Isabelle settings like this:
+\begin{ttbox}
+TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
+\end{ttbox}
+This is known to work with \textsl{teTeX} (version 1.0 or later).
+
+
+\subsubsection*{Examples}
+
+Invoking \texttt{isatool latex} by hand may be occasionally useful when
+debugging failed attempts of the automatic document preparation stage of
+batch-mode Isabelle. The abortive process leaves the sources at a certain
+place within \texttt{ISABELLE_BROWSER_INFO}, see the runtime error message for
+details. This enables users to inspect {\LaTeX} runs in further detail, e.g.\
+like this:
+
+\begin{ttbox}
+ cd ~/isabelle/browser_info/HOL/Test/document
+ isatool latex -o pdf
+\end{ttbox}
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"