doc-src/System/present.tex
 author wenzelm Mon Aug 28 13:52:38 2000 +0200 (2000-08-28) changeset 9695 ec7d7f877712 parent 9237 161fb7f00414 child 10564 42f41f966db4 permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     1

     2 %% $Id$

     3

     4 \chapter{Presenting theories}

     5

     6 Isabelle provides several ways to present the outcome of formal developments,

     7 including WWW-based browsable libraries or actual printable documents.

     8 Presentation is centered around the concept of \emph{logic sessions}.  The

     9 global session structure is that of a tree, with Isabelle \texttt{Pure} at its

    10 root, further object-logics derived (e.g.\ \texttt{HOLCF} from \texttt{HOL},

    11 and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf

    12 positions.  The latter usually do not have a separate {\ML} image.

    13

    14 The \texttt{usedir} and \texttt{mkdir} utilities provide the prime means for

    15 managing Isabelle sessions, including proper setup for presentation (see

    16 \S\ref{sec:tool-usedir} and \S\ref{sec:tool-mkdir}).

    17

    18

    19 \section{Generating theory browsing information} \label{sec:info}

    20 \index{theory browsing information|bold}

    21

    22 As a side-effect of running a logic sessions, Isabelle is able to generate

    23 theory browsing information, including HTML documents that show a theory's

    24 definition, the theorems proved in its ML file and the relationship with its

    25 ancestors and descendants.  Besides the HTML file that is generated for every

    26 theory, Isabelle stores links to all theories in an index file. These indexes

    27 are linked with other indexes to represent the overall tree structure of logic

    28 sessions.

    29

    30 Isabelle also generates graph files that represent the theory hierarchy of a

    31 logic.  There is a graph browser Java applet embedded in the generated HTML

    32 pages, and also a stand-alone application that allows browsing theory graphs

    33 without having to start a WWW browser first.  The latter version also includes

    34 features such as generating {\sc PostScript} files, which are not available in

    35 the applet version.  See \S\ref{sec:browse} for further information.

    36

    37 \medskip

    38

    39 In order to let Isabelle generate theory browsing information, simply append

    40 \texttt{-i true}'' to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before

    41 making a logic.  For example, in order to do this for FOL, add this to your

    42 Isabelle settings file

    43 \begin{ttbox}

    44 ISABELLE_USEDIR_OPTIONS="-i true"

    45 \end{ttbox}

    46 and then change into the \texttt{src/FOL} directory of the Isabelle

    47 distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.

    48

    49 Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual

    50 printable documents.  These are prepared automatically as well if enabled like

    51 this, using the \texttt{-d} option

    52 \begin{ttbox}

    53 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"

    54 \end{ttbox}

    55 See \S\ref{sec:tool-document} for further information on Isabelle document

    56 preparation.

    57

    58 \bigskip The theory browsing information is stored within the directory

    59 determined by the \settdx{ISABELLE_BROWSER_INFO} setting.  The

    60 \texttt{index.html} file located there provides an entry point to all standard

    61 Isabelle logics.  A complete HTML version of all object-logics and examples of

    62 the Isabelle distribution is available at

    63 \begin{center}\small

    64   \begin{tabular}{l}

    65     \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\

    66     \url{http://isabelle.in.tum.de/library/} \\

    67   \end{tabular}

    68 \end{center}

    69

    70 \medskip

    71

    72 The generated HTML document of any theory includes all theorems proved in the

    73 corresponding {\ML} file, provided these have been stored properly via

    74 \ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm},

    75 \ttindex{bind_thms} or \ttindex{store_thm} (see also \cite{isabelle-ref}).

    76 Section headings may be included in the presentation via the {\ML} function

    77 \begin{ttbox}\index{*section}

    78 section: string -> unit

    79 \end{ttbox}

    80

    81 \medskip

    82

    83 In order to present your own theories on the web, simply copy the

    84 corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW

    85 server, after having generated browser info like this:

    86 \begin{ttbox}

    87 isatool usedir -i true HOL Foo

    88 \end{ttbox}

    89 This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file

    90 to load all your theories, and HOL is your parent logic image.  Ideally,

    91 theory browser information would have been generated for HOL already.

    92

    93 Alternatively, one may specify an external link to an existing body of HTML

    94 data by giving \texttt{usedir} a \texttt{-P} option like this:

    95 \begin{ttbox}

    96 isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo

    97 \end{ttbox}

    98

    99 \medskip For production use, the \texttt{usedir} tool is usually invoked in an

   100 appropriate \texttt{IsaMakefile}, via the Isabelle \texttt{make} utility.

   101 There is a separate \texttt{mkdir} tool to provide easy setup of all this,

   102 with only minimal manual editing required.

   103 \begin{ttbox}

   104 isatool mkdir -d Foo

   105 edit Foo/ROOT.ML

   106 isatool make

   107 \end{ttbox}

   108 See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session

   109 directories, including the setup for documents.

   110

   111

   112 \section{Browsing theory graphs} \label{sec:browse}

   113 \index{theory graph browser|bold}

   114

   115 The graph browser is a tool for visualizing dependency graphs. Certain nodes

   116 of the graph (i.e.~theories) can be grouped together in directories'', whose

   117 contents may be hidden, thus enabling the user to filter out irrelevant

   118 information.  The browser is written in Java, it can be used both as a

   119 stand-alone application and as an applet.

   120

   121

   122 \subsection{Invoking the graph browser}

   123

   124 The stand-alone version of the graph browser is wrapped up as an

   125 Isabelle tool called \tooldx{browser}:

   126 \begin{ttbox}

   127 Usage: browser [OPTIONS] [GRAPHFILE]

   128

   129   Options are:

   130     -d           delete file after use

   131 \end{ttbox}

   132 When no filename is specified, the browser automatically changes to the

   133 directory \texttt{ISABELLE_BROWSER_INFO}.

   134

   135 \medskip The applet version of the browser can be invoked by opening the {\tt

   136   index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your

   137 Web browser and selecting the version including theory graph browser''.

   138 There is also a link to the corresponding theory graph in every logic's {\tt

   139   index.html} file.

   140

   141

   142 \subsection{Using the graph browser}

   143

   144 The browser's main window, which is shown in figure

   145 \ref{browserwindow}, consists of two sub-windows: In the left

   146 sub-window, the directory tree is displayed. The graph itself is

   147 displayed in the right sub-window.

   148 \begin{figure}[ht]

   149   \includegraphics[width=\textwidth]{browser_screenshot}

   150   \caption{\label{browserwindow} Browser main window}

   151 \end{figure}

   152

   153

   154 \subsubsection*{The directory tree window}

   155

   156 We describe the usage of the directory browser and the meaning of the

   157 different items in the browser window.

   158 \begin{itemize}

   159

   160 \item A red arrow before a directory name indicates that the directory

   161   is currently folded'', i.e.~the nodes in this directory are

   162   collapsed to one single node. In the right sub-window, the names of

   163   nodes corresponding to folded directories are enclosed in square

   164   brackets and displayed in red color.

   165

   166 \item A green downward arrow before a directory name indicates that

   167   the directory is currently unfolded''. It can be folded by

   168   clicking on the directory name.  Clicking on the name for a second

   169   time unfolds the directory again.  Alternatively, a directory can

   170   also be unfolded by clicking on the corresponding node in the right

   171   sub-window.

   172

   173 \item Blue arrows stand before ordinary node names. When clicking on such a

   174   name (i.e.\ that of a theory), the graph display window focuses to the

   175   corresponding node. Double clicking invokes a text viewer window in which

   176   the contents of the theory file are displayed.

   177

   178 \end{itemize}

   179

   180

   181 \subsubsection*{The graph display window}

   182

   183 When pointing on an ordinary node, an upward and a downward arrow is

   184 shown.  Initially, both of these arrows are green. Clicking on the

   185 upward or downward arrow collapses all predecessor or successor nodes,

   186 respectively. The arrow's color then changes to red, indicating that

   187 the predecessor or successor nodes are currently collapsed. The node

   188 corresponding to the collapsed nodes has the name {\tt [....]}''. To

   189 uncollapse the nodes again, simply click on the red arrow or on the

   190 node with the name {\tt [....]}''. Similar to the directory browser,

   191 the contents of theory files can be displayed by double clicking on

   192 the corresponding node.

   193

   194

   195 \subsubsection*{The File'' menu}

   196

   197 Please note that due to Java security restrictions this menu is not

   198 available in the applet version. The meaning of the menu items is as

   199 follows:

   200 \begin{description}

   201

   202 \item[Open \dots] Open a new graph file.

   203

   204 \item[Export to PostScript] Outputs the current graph in {\sc

   205     PostScript} format, appropriately scaled to fit on one single

   206   sheet of paper.  The resulting file can be printed directly.

   207

   208 \item[Export to EPS] Outputs the current graph in Encapsulated {\sc

   209     PostScript} format. The resulting file can be included in other

   210   documents.

   211

   212 \item[Quit] Quit the graph browser.

   213

   214 \end{description}

   215

   216

   217 \subsection*{*Syntax of graph definition files}

   218

   219 A graph definition file has the following syntax:

   220 \begin{eqnarray*}

   221   \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\

   222   vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]

   223   \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *

   224 \end{eqnarray*}

   225

   226 The meaning of the items in a vertex description is as follows:

   227 \begin{description}

   228

   229 \item[vertexname] The name of the vertex.

   230

   231 \item[vertexID] The vertex identifier. Note that there may be two

   232   vertices with equal names, whereas identifiers must be unique.

   233

   234 \item[dirname] The name of the directory'' the vertex should be

   235   placed in.  A {\tt +}'' sign after {\it dirname} indicates that

   236   the nodes in the directory are initially visible. Directories are

   237   initially invisible by default.

   238

   239 \item[path] The path of the corresponding theory file. This is

   240   specified relatively to the path of the graph definition file.

   241

   242 \item[List of successor/predecessor nodes] A {\tt <}'' sign before

   243   the list means that successor nodes are listed, a {\tt >}'' sign

   244   means that predecessor nodes are listed. If neither {\tt <}'' nor

   245   {\tt >}'' is found, the browser assumes that successor nodes are

   246   listed.

   247

   248 \end{description}

   249

   250

   251 \section{Preparing Isabelle session documents --- \texttt{isatool document}}

   252 \label{sec:tool-document}

   253

   254 The \tooldx{document} utility prepares logic session documents, processing the

   255 sources both as provided by the user and generated by Isabelle.  Its usage is:

   256 \begin{ttbox}

   257 Usage: document [OPTIONS] [DIR]

   258

   259   Options are:

   260     -c           cleanup -- be aggressive in removing old stuff

   261     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,

   262                  ps.gz, pdf

   263

   264   Prepare the theory session document in DIR (default 'document')

   265   producing the specified output format.

   266 \end{ttbox}

   267 This tool is usually run automatically as part of the corresponding session,

   268 provided document preparation has been enabled (cf.\ the \texttt{-d} option of

   269 the \texttt{usedir} utility, \S\ref{sec:tool-usedir}).  It may be manually

   270 invoked on the generated browser information document output as well.

   271

   272 \medskip Document preparation requires a properly setup \texttt{document}''

   273 directory within the logic session sources.  This directory is supposed to

   274 contain all the files needed to produce the final document --- apart from the

   275 actual theories which are generated by Isabelle.

   276

   277 \medskip For simple documents, the \texttt{document} tool is smart enough to

   278 create any of the output formats, taking \texttt{root.tex} supplied by the

   279 user as a starting point.  This even includes multiple runs of {\LaTeX} to

   280 accommodate references and bibliographies (the latter assumes

   281 \texttt{root.bib} within the same directory).

   282

   283 For complex documents, a separate \texttt{IsaMakefile} may be given instead.

   284 It should provide targets for any admissible document format; these have to

   285 produce corresponding output files named after \texttt{root} as well, e.g.\

   286 \texttt{root.dvi} for target format \texttt{dvi}.

   287

   288 \medskip When running the session, Isabelle copies the original

   289 \texttt{document} directory into its proper place within

   290 \texttt{ISABELLE_BROWSER_INFO} according to the session path.  Then, for any

   291 processed theory $A$ some {\LaTeX} source is generated and put there as

   292 $A$\texttt{.tex}.  Furthermore, a list of all generated theory files is put

   293 into \texttt{session.tex}.  Typically, the root {\LaTeX} file provided by the

   294 user would include \texttt{session.tex} to get a document containing all the

   295 theories.

   296

   297 The {\LaTeX} versions of the theories require some macros defined in

   298 \texttt{isabelle.sty} as distributed with Isabelle.  Doing

   299 \verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;

   300 the underlying Isabelle \texttt{latex} utility already includes an appropriate

   301 {\TeX} inputs path.

   302

   303 If the text contains any references to Isabelle symbols (such as

   304 \verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.

   305 This package contains a standard set of {\LaTeX} macro definitions

   306 \verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>,.  The user may

   307 refer to further symbols as well, simply by providing {\LaTeX} macros of the

   308 same sort.

   309

   310 For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail

   311 images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to

   312 do so even without using PDF~\LaTeX.

   313

   314 \medskip As a final step, \texttt{isatool document -c} is run on the resulting

   315 \texttt{document} directory.  Thus the actual output document is built and

   316 installed in its proper place (as linked by the session's

   317 \texttt{index.html}).  The generated sources are deleted after successful run

   318 of {\LaTeX} and friends.  Note that a copy of the sources may be retained by

   319 passing an option \texttt{-D} to the \texttt{usedir} utility when running the

   320 session (see also \S\ref{sec:tool-usedir}).

   321

   322

   323 \section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}

   324 \label{sec:tool-latex}

   325

   326 The \tooldx{latex} utility provides the basic interface for Isabelle document

   327 preparation.  Its usage is:

   328 \begin{ttbox}

   329 Usage: latex [OPTIONS] [FILE]

   330

   331   Options are:

   332     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,

   333                  ps.gz, pdf, bbl, png, sty

   334

   335   Run LaTeX (and related tools) on FILE (default root.tex),

   336   producing the specified output format.

   337 \end{ttbox}

   338 Appropriate {\LaTeX}-related programs are run on the input file, according to

   339 the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},

   340 \texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).

   341 The actual commands are determined from the settings environment

   342 (\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).

   343

   344 The \texttt{sty} output format causes the Isabelle style files to be updated

   345 from the distribution.  This is useful in special situations where the

   346 document sources are to be processed another time by separate tools (cf.\

   347 option \texttt{-D} of the \texttt{usedir} utility, see

   348 \S\ref{sec:tool-usedir}).

   349

   350 It is important to note that the {\LaTeX} inputs file space has to be properly

   351 setup to include the Isabelle styles.  Usually, this may be done by modifying

   352 the \settdx{TEXINPUTS} variable in settings like this:

   353 \begin{ttbox}

   354 TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"

   355 \end{ttbox}

   356 This is known to work with recent versions of the \textsl{teTeX} distribution.

   357

   358

   359 \section{Creating Isabelle session directories --- \texttt{isatool mkdir}}

   360 \label{sec:tool-mkdir}

   361

   362 The \tooldx{mkdir} utility prepares Isabelle session source directories,

   363 including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML}

   364 and an optional \texttt{document} directory.  Its usage is:

   365 \begin{ttbox}

   366 Usage: mkdir [OPTIONS] [LOGIC] NAME

   367

   368   Options are:

   369     -I FILE      alternative IsaMakefile output

   370     -P           include parent logic target

   371     -b           setup build mode (session outputs heap image)

   372     -d           setup document

   373

   374   Prepare session directory, including IsaMakefile, document etc.

   375   with parent LOGIC (default ISABELLE_LOGIC=\\$ISABELLE_LOGIC)

   376 \end{ttbox}

   377

   378 The \texttt{mkdir} tool is conservative in the sense that any existing

   379 \texttt{IsaMakefile} etc.\ is left unchanged.  Thus it is safe to invoke it

   380 experimentally, with varying options.

   381

   382 Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile}

   383 incrementally --- manual changes are required for multiple sub-sessions.  On

   384 order to get an initial working session, the only editing needed is to add

   385 appropriate \texttt{use_thy} calls to the generated \texttt{ROOT.ML} file.

   386

   387

   388 \subsection*{Options}

   389

   390 The \texttt{-I} option specifies an alternative to \texttt{IsaMakefile} for

   391 dependencies.  Note that \texttt{-}'' refers to \emph{stdout}, i.e.\

   392 \texttt{-I-}'' provides an easy way to peek at \texttt{mkdir}'s idea of

   393 \texttt{make} setup required for some particular of Isabelle session.

   394

   395 \medskip The \texttt{-P} option includes a target for the parent

   396 \texttt{LOGIC} session in the generated \texttt{IsaMakefile}.  The

   397 corresponding sources are assumed to be located within the Isabelle

   398 distribution.

   399

   400 \medskip The \texttt{-b} option sets up the current directory as the base for

   401 a new session that provides an actual logic image, as opposed to one that only

   402 runs several theories based on an existing image.  Note that in the latter

   403 case, everything except \texttt{IsaMakefile} would be placed into a separate

   404 directory \texttt{NAME}, rather than the current one.  See

   405 \S\ref{sec:tool-usedir} for further information on \emph{build mode} vs.\

   406 \emph{example mode} of the \texttt{usedir} utility.

   407

   408 \medskip The \texttt{-d} option creates a \texttt{document} directory with a

   409 minimal \texttt{root.tex} file, which is sufficient to get all theories pretty

   410 printed in the order of appearance.  See \S\ref{sec:tool-document} for further

   411 information on Isabelle document preparation.

   412

   413

   414 \subsection*{Examples}

   415

   416 The standard setup of a single example session'' based on the default logic,

   417 with proper document generation is generated like this:

   418 \begin{ttbox}

   419 isatool mkdir -d Foo

   420 \end{ttbox}

   421 \noindent The theory sources should be put into the \texttt{Foo} directory, and its

   422 \texttt{ROOT.ML} should be edited to load all required theories.  Invoking

   423 \texttt{isatool make} would now run the whole session, generating browser

   424 information and the document automatically.  The \texttt{IsaMakefile} is

   425 usually tuned manually later, e.g.\ adding actual source dependencies, or

   426 changing the options passed to \texttt{usedir}.

   427

   428

   429 \section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}

   430

   431 The \tooldx{usedir} utility builds object-logic images, or runs example

   432 sessions based on existing logics. Its usage is:

   433 \begin{ttbox}

   434 Usage: usedir [OPTIONS] LOGIC NAME

   435

   436   Options are:

   437     -D PATH      dump generated document sources into PATH

   438     -P PATH      set path for remote theory browsing information

   439     -b           build mode (output heap image, using current dir)

   440     -c BOOL      tell ML system to compress output image (default true)

   441     -d FORMAT    build document as FORMAT (default false)

   442     -i BOOL      generate theory browsing information,

   443                  i.e. HTML / graph data (default false)

   444     -r           reset session path

   445     -s NAME      override session NAME

   446

   447   Build object-logic or run examples. Also creates browsing

   448   information (HTML etc.) according to settings.

   449

   450   ISABELLE_USEDIR_OPTIONS=

   451 \end{ttbox}

   452

   453 Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is

   454 implicitly prefixed to \emph{any} \texttt{usedir} call. Since the

   455 \ttindex{IsaMakefile}s of all object-logics distributed with Isabelle just

   456 invoke \texttt{usedir} for the real work, one may control compilation options

   457 globally via above variable. In particular, generation of \rmindex{HTML}

   458 browsing information and document preparation is controlled here.

   459

   460

   461 \subsection*{Options}

   462

   463 Basically, there are two different modes of operation: \emph{build mode}

   464 (enabled through the \texttt{-b} option) and \emph{example mode} (default).

   465

   466 Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input

   467 image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command

   468 line. This will be a batch session, running \texttt{ROOT.ML} from the current

   469 directory and then quitting.  It is assumed that \texttt{ROOT.ML} contains all

   470 {\ML} commands required to build the logic.

   471

   472 In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}

   473 and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}.

   474 It assumes that this file contains appropriate {\ML} commands to run the

   475 desired examples.

   476

   477 \medskip The \texttt{-i} option controls theory browser data generation. It

   478 may be explicitly turned on or off --- as usual, the last occurrence of

   479 \texttt{-i} on the command line wins.  The \texttt{-P} option specifies a path

   480 (or actual URL) to be prefixed to any \emph{non-local} reference of existing

   481 theories.  Thus user sessions may easily link to existing Isabelle libraries

   482 already present on the WWW.

   483

   484 \medskip The \texttt{-d} option controls document preparation.  Valid

   485 arguments are \texttt{false} (do not prepare any document; this is default),

   486 or any of \texttt{dvi}, \texttt{dvi.gz}, \texttt{ps}, \texttt{ps.gz},

   487 \texttt{pdf}.  The logic session has to provide a properly setup

   488 \texttt{document} directory.  See \S\ref{sec:tool-document} and

   489 \S\ref{sec:tool-latex} for more details.

   490

   491 \medskip The \texttt{-D} option causes the generated document sources to be

   492 dumped at location \texttt{PATH}, which is relative to the session's main

   493 directory.  For example, \texttt{-D document} would leave a copy of the

   494 {\LaTeX} sources in the actual document directory.  Thus the Isabelle

   495 \texttt{document} or \texttt{latex} tools may be run later, facilitating much

   496 easier debugging of {\LaTeX} errors, for example.  Note that a copy of the

   497 Isabelle style files will be placed in \texttt{PATH} as well.

   498

   499 \medskip Any \texttt{usedir} session is named by some \emph{session

   500   identifier}. These accumulate, documenting the way sessions depend on

   501 others. For example, consider \texttt{Pure/FOL/ex}, which refers to the

   502 examples of FOL, which in turn is built upon Pure.

   503

   504 The current session's identifier is by default just the base name of the

   505 \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in

   506 example mode). This may be overridden explicitly via the \texttt{-s} option.

   507

   508

   509 \subsection*{Examples}

   510

   511 Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's

   512 object-logics as a model for your own developments.  For example, see

   513 \texttt{src/FOL/IsaMakefile}.  The Isabelle \texttt{mkdir} tool (see

   514 \S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation

   515 of \texttt{usedir} as well.

   516

   517

   518 %%% Local Variables:

   519 %%% mode: latex

   520 %%% TeX-master: "system"

   521 %%% End: