--- a/src/Doc/System/Basics.thy Mon Oct 12 17:11:17 2015 +0200
+++ b/src/Doc/System/Basics.thy Mon Oct 12 18:18:48 2015 +0200
@@ -192,7 +192,7 @@
Note that the following bash expression (including the quotes)
prefers the 64 bit platform, if that is available:
- @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}
+ @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
\item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
@@ -298,19 +298,13 @@
For example, the following setting allows to refer to files within
the component later on, without having to hardwire absolute paths:
-
-\begin{ttbox}
-MY_COMPONENT_HOME="$COMPONENT"
-\end{ttbox}
+ @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
Components can also add to existing Isabelle settings such as
@{setting_def ISABELLE_TOOLS}, in order to provide
component-specific tools that can be invoked by end-users. For
example:
-
-\begin{ttbox}
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-\end{ttbox}
+ @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
\<^item> @{verbatim "etc/components"} holds a list of further
sub-components of the same structure. The directory specifications
@@ -328,9 +322,7 @@
@{verbatim init_component} shell function in the @{verbatim "etc/settings"}
script of @{verbatim "$ISABELLE_HOME_USER"} (or any other component
directory). For example:
-\begin{ttbox}
-init_component "$HOME/screwdriver-2.0"
-\end{ttbox}
+ @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
This is tolerant wrt.\ missing component directories, but might
produce a warning.
@@ -339,10 +331,7 @@
More complex situations may be addressed by initializing
components listed in a given catalog file, relatively to some base
directory:
-
-\begin{ttbox}
-init_components "$HOME/my_component_store" "some_catalog_file"
-\end{ttbox}
+ @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
The component directories listed in the catalog file are treated as
relative to the given base directory.
@@ -360,9 +349,8 @@
Isabelle logic sessions --- either interactively or in batch mode.
It provides an abstraction over the underlying ML system, and over
the actual heap file locations. Its usage is:
-
-\begin{ttbox}
-Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
+ @{verbatim [display]
+\<open>Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
Options are:
-O system options from given YXML file
@@ -375,11 +363,10 @@
-r open heap file read-only
-w reset write permissions on OUTPUT
- INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
+ INPUT (default "$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
These are either names to be searched in the Isabelle path, or
actual file names (containing at least one /).
- If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
-\end{ttbox}
+ If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.\<close>}
Input files without path specifications are looked up in the
@{setting ISABELLE_PATH} setting, which may consist of multiple
@@ -460,40 +447,32 @@
text \<open>
Run an interactive session of the default object-logic (as specified
by the @{setting ISABELLE_LOGIC} setting) like this:
-\begin{ttbox}
-isabelle_process
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle_process\<close>}
Usually @{setting ISABELLE_LOGIC} refers to one of the standard
logic images, which are read-only by default. A writable session
--- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
may be invoked as follows:
-\begin{ttbox}
-isabelle_process HOL Test
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle_process HOL Test\<close>}
+
Ending this session normally (e.g.\ by typing control-D) dumps the
whole ML system state into @{verbatim Test} (be prepared for more
than 100\,MB):
The @{verbatim Test} session may be continued later (still in
- writable state) by:
-\begin{ttbox}
-isabelle_process Test
-\end{ttbox}
+ writable state) by: @{verbatim [display] \<open>isabelle_process Test\<close>}
+
A read-only @{verbatim Test} session may be started by:
-\begin{ttbox}
-isabelle_process -r Test
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle_process -r Test\<close>}
\<^bigskip>
The next example demonstrates batch execution of Isabelle.
We retrieve the @{verbatim Main} theory value from the theory loader
within ML (observe the delicate quoting rules for the Bash shell
vs.\ ML):
-\begin{ttbox}
-isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL\<close>}
+
Note that the output text will be interspersed with additional junk
messages by the ML runtime environment. The @{verbatim "-W"} option
allows to communicate with the Isabelle process via an external
@@ -506,15 +485,13 @@
text \<open>
All Isabelle related tools and interfaces are called via a common
wrapper --- @{executable isabelle}:
-
-\begin{ttbox}
-Usage: isabelle TOOL [ARGS ...]
+ @{verbatim [display]
+\<open>Usage: isabelle TOOL [ARGS ...]
Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
Available tools:
- \dots
-\end{ttbox}
+ ...\<close>}
In principle, Isabelle tools are ordinary executable scripts that
are run within the Isabelle settings environment, see
@@ -530,20 +507,13 @@
text \<open>Show the list of available documentation of the Isabelle
distribution:
-
-\begin{ttbox}
- isabelle doc
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle doc\<close>}
View a certain document as follows:
-\begin{ttbox}
- isabelle doc system
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle doc system\<close>}
Query the Isabelle settings environment:
-\begin{ttbox}
- isabelle getenv ISABELLE_HOME_USER
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
\<close>
end
\ No newline at end of file
--- a/src/Doc/System/Misc.thy Mon Oct 12 17:11:17 2015 +0200
+++ b/src/Doc/System/Misc.thy Mon Oct 12 18:18:48 2015 +0200
@@ -24,14 +24,14 @@
text \<open>The stand-alone version of the graph browser is wrapped up as
@{tool_def browser}:
-\begin{ttbox}
-Usage: isabelle browser [OPTIONS] [GRAPHFILE]
+ @{verbatim [display]
+\<open>Usage: isabelle browser [OPTIONS] [GRAPHFILE]
Options are:
-b Admin/build only
-c cleanup -- remove GRAPHFILE after use
- -o FILE output to FILE (ps, eps, pdf)
-\end{ttbox}
+ -o FILE output to FILE (ps, eps, pdf)\<close>}
+
When no file name is specified, the browser automatically changes to
the directory @{setting ISABELLE_BROWSER_INFO}.
@@ -186,8 +186,8 @@
text \<open>
The @{tool_def components} tool resolves Isabelle components:
-\begin{ttbox}
-Usage: isabelle components [OPTIONS] [COMPONENTS ...]
+ @{verbatim [display]
+\<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...]
Options are:
-I init user settings
@@ -199,8 +199,7 @@
Resolve Isabelle components via download and installation.
COMPONENTS are identified via base name.
- ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
-\end{ttbox}
+ ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"\<close>}
Components are initialized as described in \secref{sec:components}
in a permissive manner, which can mark components as ``missing''.
@@ -236,8 +235,8 @@
text \<open>
The @{tool_def console} tool runs the Isabelle process with raw ML console:
-\begin{ttbox}
-Usage: isabelle console [OPTIONS]
+ @{verbatim [display]
+\<open>Usage: isabelle console [OPTIONS]
Options are:
-d DIR include session directory
@@ -248,8 +247,7 @@
-s system build mode for session image
Run Isabelle process with raw ML console and line editor
- (default ISABELLE_LINE_EDITOR).
-\end{ttbox}
+ (default ISABELLE_LINE_EDITOR).\<close>}
The @{verbatim "-l"} option specifies the logic session name. By default,
its heap image is checked and built on demand, but the option @{verbatim
@@ -277,11 +275,10 @@
text \<open>The @{tool_def display} tool displays documents in DVI or PDF
format:
-\begin{ttbox}
-Usage: isabelle display DOCUMENT
+ @{verbatim [display]
+\<open>Usage: isabelle display DOCUMENT
- Display DOCUMENT (in DVI or PDF format).
-\end{ttbox}
+ Display DOCUMENT (in DVI or PDF format).\<close>}
\<^medskip>
The settings @{setting DVI_VIEWER} and @{setting
@@ -296,11 +293,11 @@
text \<open>
The @{tool_def doc} tool displays Isabelle documentation:
-\begin{ttbox}
-Usage: isabelle doc [DOC ...]
+ @{verbatim [display]
+\<open>Usage: isabelle doc [DOC ...]
- View Isabelle documentation.
-\end{ttbox}
+ View Isabelle documentation.\<close>}
+
If called without arguments, it lists all available documents. Each
line starts with an identifier, followed by a short description. Any
of these identifiers may be specified as arguments, in order to
@@ -322,9 +319,7 @@
The command-line arguments are that of the underlying version of
@{verbatim env}. For example, the following invokes an instance of
the GNU Bash shell within the Isabelle environment:
-\begin{alltt}
- isabelle env bash
-\end{alltt}
+ @{verbatim [display] \<open>isabelle env bash\<close>}
\<close>
@@ -333,8 +328,8 @@
text \<open>The Isabelle settings environment --- as provided by the
site-default and user-specific settings files --- can be inspected
with the @{tool_def getenv} tool:
-\begin{ttbox}
-Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
+ @{verbatim [display]
+\<open>Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
Options are:
-a display complete environment
@@ -342,8 +337,7 @@
-d FILE dump complete environment to FILE
(null terminated entries)
- Get value of VARNAMES from the Isabelle settings.
-\end{ttbox}
+ Get value of VARNAMES from the Isabelle settings.\<close>}
With the @{verbatim "-a"} option, one may inspect the full process
environment that Isabelle related programs are run in. This usually
@@ -362,16 +356,12 @@
text \<open>Get the location of @{setting ISABELLE_HOME_USER} where
user-specific information is stored:
-\begin{ttbox}
-isabelle getenv ISABELLE_HOME_USER
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
\<^medskip>
Get the value only of the same settings variable, which is
-particularly useful in shell scripts:
-\begin{ttbox}
-isabelle getenv -b ISABELLE_OUTPUT
-\end{ttbox}
+ particularly useful in shell scripts:
+ @{verbatim [display] \<open>isabelle getenv -b ISABELLE_OUTPUT\<close>}
\<close>
@@ -382,16 +372,15 @@
distribution directory, probably indirectly by the shell through its
@{setting PATH}. Other schemes of installation are supported by the
@{tool_def install} tool:
-\begin{ttbox}
-Usage: isabelle install [OPTIONS] BINDIR
+ @{verbatim [display]
+\<open>Usage: isabelle install [OPTIONS] BINDIR
Options are:
-d DISTDIR refer to DISTDIR as Isabelle distribution
(default ISABELLE_HOME)
Install Isabelle executables with absolute references to the
- distribution directory.
-\end{ttbox}
+ distribution directory.\<close>}
The @{verbatim "-d"} option overrides the current Isabelle
distribution directory as determined by @{setting ISABELLE_HOME}.
@@ -411,15 +400,14 @@
text \<open>The @{tool_def logo} tool creates instances of the generic
Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
-\begin{ttbox}
-Usage: isabelle logo [OPTIONS] XYZ
+ @{verbatim [display]
+\<open>Usage: isabelle logo [OPTIONS] XYZ
Create instance XYZ of the Isabelle logo (as EPS and PDF).
Options are:
-n NAME alternative output base name (default "isabelle_xyx")
- -q quiet mode
-\end{ttbox}
+ -q quiet mode\<close>}
Option @{verbatim "-n"} specifies an altenative (base) name for the
generated files. The default is @{verbatim "isabelle_"}@{text xyz}
@@ -437,14 +425,13 @@
text \<open>
The @{tool_def version} tool displays Isabelle version information:
-\begin{ttbox}
-Usage: isabelle version [OPTIONS]
+ @{verbatim [display]
+\<open>Usage: isabelle version [OPTIONS]
Options are:
-i short identification (derived from Mercurial id)
- Display Isabelle version information.
-\end{ttbox}
+ Display Isabelle version information.\<close>}
\<^medskip>
The default is to output the full version string of the
--- a/src/Doc/System/Presentation.thy Mon Oct 12 17:11:17 2015 +0200
+++ b/src/Doc/System/Presentation.thy Mon Oct 12 18:18:48 2015 +0200
@@ -75,10 +75,7 @@
The easiest way to let Isabelle generate theory browsing information
for existing sessions is to invoke @{tool build} with suitable
options:
-
-\begin{ttbox}
-isabelle build -o browser_info -v -c FOL
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>}
The presentation output will appear in @{verbatim
"$ISABELLE_BROWSER_INFO/FOL/FOL"} as reported by the above verbose
@@ -87,9 +84,7 @@
Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file
"~~/src/HOL/Library"}) also provide actual printable documents.
These are prepared automatically as well if enabled like this:
-\begin{ttbox}
-isabelle build -o browser_info -o document=pdf -v -c HOL-Library
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
Enabling both browser info and document preparation simultaneously
causes an appropriate ``document'' link to be included in the HTML
@@ -111,15 +106,14 @@
text \<open>The @{tool_def mkroot} tool configures a given directory as
session root, with some @{verbatim ROOT} file and optional document
source directory. Its usage is:
-\begin{ttbox}
-Usage: isabelle mkroot [OPTIONS] [DIR]
+ @{verbatim [display]
+\<open>Usage: isabelle mkroot [OPTIONS] [DIR]
Options are:
-d enable document preparation
-n NAME alternative session name (default: DIR base name)
- Prepare session root DIR (default: current directory).
-\end{ttbox}
+ Prepare session root DIR (default: current directory).\<close>}
The results are placed in the given directory @{text dir}, which
refers to the current directory by default. The @{tool mkroot} tool
@@ -147,27 +141,22 @@
text \<open>Produce session @{verbatim Test} (with document preparation)
within a separate directory of the same name:
-\begin{ttbox}
-isabelle mkroot -d Test && isabelle build -D Test
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
\<^medskip>
Upgrade the current directory into a session ROOT with
document preparation, and build it:
-\begin{ttbox}
-isabelle mkroot -d && isabelle build -D .
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
\<close>
-section \<open>Preparing Isabelle session documents
- \label{sec:tool-document}\<close>
+section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
text \<open>The @{tool_def document} tool prepares logic session
documents, processing the sources as provided by the user and
generated by Isabelle. Its usage is:
-\begin{ttbox}
-Usage: isabelle document [OPTIONS] [DIR]
+ @{verbatim [display]
+\<open>Usage: isabelle document [OPTIONS] [DIR]
Options are:
-c cleanup -- be aggressive in removing old stuff
@@ -176,8 +165,8 @@
-t TAGS specify tagged region markup
Prepare the theory session document in DIR (default 'document')
- producing the specified output format.
-\end{ttbox}
+ producing the specified output format.\<close>}
+
This tool is usually run automatically as part of the Isabelle build
process, provided document preparation has been enabled via suitable
options. It may be manually invoked on the generated browser
@@ -282,16 +271,15 @@
text \<open>The @{tool_def latex} tool provides the basic interface for
Isabelle document preparation. Its usage is:
-\begin{ttbox}
-Usage: isabelle latex [OPTIONS] [FILE]
+ @{verbatim [display]
+\<open>Usage: isabelle latex [OPTIONS] [FILE]
Options are:
-o FORMAT specify output format: pdf (default), dvi,
bbl, idx, sty, syms
Run LaTeX (and related tools) on FILE (default root.tex),
- producing the specified output format.
-\end{ttbox}
+ producing the specified output format.\<close>}
Appropriate {\LaTeX}-related programs are run on the input file,
according to the given output format: @{executable latex},
@@ -320,10 +308,9 @@
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 getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
- isabelle latex -o pdf
-\end{ttbox}
+ @{verbatim [display]
+\<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
+isabelle latex -o pdf\<close>}
\<close>
end
\ No newline at end of file
--- a/src/Doc/System/Scala.thy Mon Oct 12 17:11:17 2015 +0200
+++ b/src/Doc/System/Scala.thy Mon Oct 12 18:18:48 2015 +0200
@@ -30,9 +30,7 @@
For example, the following command-line invokes the main method of
class @{verbatim isabelle.GUI_Setup}, which opens a windows with
some diagnostic information about the Isabelle environment:
-\begin{alltt}
- isabelle java isabelle.GUI_Setup
-\end{alltt}
+ @{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
\<close>
@@ -43,13 +41,12 @@
are that of the underlying Scala version.
This allows to interact with Isabelle/Scala in TTY mode like this:
-\begin{alltt}
- isabelle scala
- scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
- scala> val options = isabelle.Options.init()
- scala> options.bool("browser_info")
- scala> options.string("document")
-\end{alltt}
+ @{verbatim [display]
+\<open>isabelle scala
+scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
+scala> val options = isabelle.Options.init()
+scala> options.bool("browser_info")
+scala> options.string("document")\<close>}
\<close>
@@ -81,14 +78,12 @@
The subsequent example assumes that the main Isabelle binaries have
been installed in some directory that is included in @{setting PATH}
(see also @{tool "install"}):
-
-\begin{alltt}
-#!/usr/bin/env isabelle_scala_script
+ @{verbatim [display]
+\<open>#!/usr/bin/env isabelle_scala_script
val options = isabelle.Options.init()
Console.println("browser_info = " + options.bool("browser_info"))
-Console.println("document = " + options.string("document"))
-\end{alltt}
+Console.println("document = " + options.string("document"))\<close>}
Alternatively the full @{file
"$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
--- a/src/Doc/System/Sessions.thy Mon Oct 12 17:11:17 2015 +0200
+++ b/src/Doc/System/Sessions.thy Mon Oct 12 18:18:48 2015 +0200
@@ -233,8 +233,8 @@
The @{tool_def options} tool prints Isabelle system options. Its
command-line usage is:
-\begin{ttbox}
-Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
+ @{verbatim [display]
+\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
Options are:
-b include $ISABELLE_BUILD_OPTIONS
@@ -243,8 +243,7 @@
-x FILE export to FILE in YXML format
Report Isabelle system options, augmented by MORE_OPTIONS given as
- arguments NAME=VAL or NAME.
-\end{ttbox}
+ arguments NAME=VAL or NAME.\<close>}
The command line arguments provide additional system options of the
form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
@@ -272,8 +271,8 @@
optional document preparation. Its command-line usage
is:\footnote{Isabelle/Scala provides the same functionality via
\texttt{isabelle.Build.build}.}
-\begin{ttbox}
-Usage: isabelle build [OPTIONS] [SESSIONS ...]
+ @{verbatim [display]
+\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-D DIR include session directory and select its sessions
@@ -299,8 +298,7 @@
ML_PLATFORM="..."
ML_HOME="..."
ML_SYSTEM="..."
- ML_OPTIONS="..."
-\end{ttbox}
+ ML_OPTIONS="..."\<close>}
\<^medskip>
Isabelle sessions are defined via session ROOT files as
@@ -402,64 +400,46 @@
text \<open>
Build a specific logic image:
-\begin{ttbox}
-isabelle build -b HOLCF
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -b HOLCF\<close>}
\<^smallskip>
Build the main group of logic images:
-\begin{ttbox}
-isabelle build -b -g main
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -b -g main\<close>}
\<^smallskip>
Provide a general overview of the status of all Isabelle
sessions, without building anything:
-\begin{ttbox}
-isabelle build -a -n -v
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
\<^smallskip>
Build all sessions with HTML browser info and PDF
document preparation:
-\begin{ttbox}
-isabelle build -a -o browser_info -o document=pdf
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
\<^smallskip>
Build all sessions with a maximum of 8 parallel prover
processes and 4 worker threads each (on a machine with many cores):
-\begin{ttbox}
-isabelle build -a -j8 -o threads=4
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
\<^smallskip>
Build some session images with cleanup of their
descendants, while retaining their ancestry:
-\begin{ttbox}
-isabelle build -b -c HOL-Algebra HOL-Word
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
\<^smallskip>
Clean all sessions without building anything:
-\begin{ttbox}
-isabelle build -a -n -c
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -a -n -c\<close>}
\<^smallskip>
Build all sessions from some other directory hierarchy,
according to the settings variable @{verbatim "AFP"} that happens to
be defined inside the Isabelle environment:
-\begin{ttbox}
-isabelle build -D '$AFP'
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
\<^smallskip>
Inform about the status of all sessions required for AFP,
without building anything yet:
-\begin{ttbox}
-isabelle build -D '$AFP' -R -v -n
-\end{ttbox}
+ @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
\<close>
end
--- a/src/Doc/System/document/root.tex Mon Oct 12 17:11:17 2015 +0200
+++ b/src/Doc/System/document/root.tex Mon Oct 12 18:18:48 2015 +0200
@@ -16,6 +16,7 @@
\isadroptag{theory}
\isabellestyle{literal}
+\def\isastylett{\footnotesize\tt}
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}