src/Doc/System/Basics.thy
author wenzelm
Tue Aug 28 18:57:32 2012 +0200 (2012-08-28)
changeset 48985 5386df44a037
parent 48937 doc-src/System/Basics.thy@e7418f8d49fe
child 49173 fa01a202399c
permissions -rw-r--r--
renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;
     1 theory Basics
     2 imports Base
     3 begin
     4 
     5 chapter {* The Isabelle system environment *}
     6 
     7 text {* This manual describes Isabelle together with related tools and
     8   user interfaces as seen from a system oriented view.  See also the
     9   \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
    10   the actual Isabelle input language and related concepts, and
    11   \emph{The Isabelle/Isar Implementation
    12   Manual}~\cite{isabelle-implementation} for the main concepts of the
    13   underlying implementation in Isabelle/ML.
    14 
    15   \medskip The Isabelle system environment provides the following
    16   basic infrastructure to integrate tools smoothly.
    17 
    18   \begin{enumerate}
    19 
    20   \item The \emph{Isabelle settings} mechanism provides process
    21   environment variables to all Isabelle executables (including tools
    22   and user interfaces).
    23 
    24   \item The raw \emph{Isabelle process} (@{executable_ref
    25   "isabelle-process"}) runs logic sessions either interactively or in
    26   batch mode.  In particular, this view abstracts over the invocation
    27   of the actual ML system to be used.  Regular users rarely need to
    28   care about the low-level process.
    29 
    30   \item The main \emph{Isabelle tool wrapper} (@{executable_ref
    31   isabelle}) provides a generic startup environment Isabelle related
    32   utilities, user interfaces etc.  Such tools automatically benefit
    33   from the settings mechanism.
    34 
    35   \end{enumerate}
    36 *}
    37 
    38 
    39 section {* Isabelle settings \label{sec:settings} *}
    40 
    41 text {*
    42   The Isabelle system heavily depends on the \emph{settings
    43   mechanism}\indexbold{settings}.  Essentially, this is a statically
    44   scoped collection of environment variables, such as @{setting
    45   ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
    46   variables are \emph{not} intended to be set directly from the shell,
    47   though.  Isabelle employs a somewhat more sophisticated scheme of
    48   \emph{settings files} --- one for site-wide defaults, another for
    49   additional user-specific modifications.  With all configuration
    50   variables in clearly defined places, this scheme is more
    51   maintainable and user-friendly than global shell environment
    52   variables.
    53 
    54   In particular, we avoid the typical situation where prospective
    55   users of a software package are told to put several things into
    56   their shell startup scripts, before being able to actually run the
    57   program. Isabelle requires none such administrative chores of its
    58   end-users --- the executables can be invoked straight away.
    59   Occasionally, users would still want to put the @{file
    60   "$ISABELLE_HOME/bin"} directory into their shell's search path, but
    61   this is not required.
    62 *}
    63 
    64 
    65 subsection {* Bootstrapping the environment \label{sec:boot} *}
    66 
    67 text {* Isabelle executables need to be run within a proper settings
    68   environment.  This is bootstrapped as described below, on the first
    69   invocation of one of the outer wrapper scripts (such as
    70   @{executable_ref isabelle}).  This happens only once for each
    71   process tree, i.e.\ the environment is passed to subprocesses
    72   according to regular Unix conventions.
    73 
    74   \begin{enumerate}
    75 
    76   \item The special variable @{setting_def ISABELLE_HOME} is
    77   determined automatically from the location of the binary that has
    78   been run.
    79   
    80   You should not try to set @{setting ISABELLE_HOME} manually. Also
    81   note that the Isabelle executables either have to be run from their
    82   original location in the distribution directory, or via the
    83   executable objects created by the @{tool install} tool.  Symbolic
    84   links are admissible, but a plain copy of the @{file
    85   "$ISABELLE_HOME/bin"} files will not work!
    86 
    87   \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
    88   @{executable_ref bash} shell script with the auto-export option for
    89   variables enabled.
    90   
    91   This file holds a rather long list of shell variable assigments,
    92   thus providing the site-wide default settings.  The Isabelle
    93   distribution already contains a global settings file with sensible
    94   defaults for most variables.  When installing the system, only a few
    95   of these may have to be adapted (probably @{setting ML_SYSTEM}
    96   etc.).
    97   
    98   \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
    99   exists) is run in the same way as the site default settings. Note
   100   that the variable @{setting ISABELLE_HOME_USER} has already been set
   101   before --- usually to something like @{verbatim
   102   "$USER_HOME/.isabelle/IsabelleXXXX"}.
   103   
   104   Thus individual users may override the site-wide defaults.  See also
   105   file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
   106   distribution.  Typically, a user settings file would contain only a
   107   few lines, just the assigments that are really changed.  One should
   108   definitely \emph{not} start with a full copy the basic @{file
   109   "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
   110   maintainance problems later, when the Isabelle installation is
   111   updated or changed otherwise.
   112   
   113   \end{enumerate}
   114 
   115   Since settings files are regular GNU @{executable_def bash} scripts,
   116   one may use complex shell commands, such as @{verbatim "if"} or
   117   @{verbatim "case"} statements to set variables depending on the
   118   system architecture or other environment variables.  Such advanced
   119   features should be added only with great care, though. In
   120   particular, external environment references should be kept at a
   121   minimum.
   122 
   123   \medskip A few variables are somewhat special:
   124 
   125   \begin{itemize}
   126 
   127   \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
   128   automatically to the absolute path names of the @{executable
   129   "isabelle-process"} and @{executable isabelle} executables,
   130   respectively.
   131   
   132   \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
   133   the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
   134   the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
   135   to its value.
   136 
   137   \end{itemize}
   138 
   139   \medskip Note that the settings environment may be inspected with
   140   the @{tool getenv} tool.  This might help to figure out the effect
   141   of complex settings scripts.  *}
   142 
   143 
   144 subsection {* Common variables *}
   145 
   146 text {*
   147   This is a reference of common Isabelle settings variables. Note that
   148   the list is somewhat open-ended. Third-party utilities or interfaces
   149   may add their own selection. Variables that are special in some
   150   sense are marked with @{text "\<^sup>*"}.
   151 
   152   \begin{description}
   153 
   154   \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform
   155   user home directory.  On Unix systems this is usually the same as
   156   @{setting HOME}, but on Windows it is the regular home directory of
   157   the user, not the one of within the Cygwin root
   158   file-system.\footnote{Cygwin itself offers another choice whether
   159   its HOME should point to the \texttt{/home} directory tree or the
   160   Windows user home.}
   161 
   162  \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
   163   top-level Isabelle distribution directory. This is automatically
   164   determined from the Isabelle executable that has been invoked.  Do
   165   not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
   166   
   167   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
   168   counterpart of @{setting ISABELLE_HOME}. The default value is
   169   relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
   170   circumstances this may be changed in the global setting file.
   171   Typically, the @{setting ISABELLE_HOME_USER} directory mimics
   172   @{setting ISABELLE_HOME} to some extend. In particular, site-wide
   173   defaults may be overridden by a private @{verbatim
   174   "$ISABELLE_HOME_USER/etc/settings"}.
   175   
   176   \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
   177   set to a symbolic identifier for the underlying hardware and
   178   operating system.  The Isabelle platform identification always
   179   refers to the 32 bit variant, even this is a 64 bit machine.  Note
   180   that the ML or Java runtime may have a different idea, depending on
   181   which binaries are actually run.
   182 
   183   \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
   184   @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
   185   on a platform that supports this; the value is empty for 32 bit.
   186   Note that the following bash expression (including the quotes)
   187   prefers the 64 bit platform, if that is available:
   188 
   189   @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}
   190 
   191   \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
   192   ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   193   names of the @{executable "isabelle-process"} and @{executable
   194   isabelle} executables, respectively.  Thus other tools and scripts
   195   need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
   196   on the current search path of the shell.
   197   
   198   \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
   199   to the name of this Isabelle distribution, e.g.\ ``@{verbatim
   200   Isabelle2012}''.
   201 
   202   \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
   203   @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
   204   ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
   205   to be used for Isabelle.  There is only a fixed set of admissable
   206   @{setting ML_SYSTEM} names (see the @{file
   207   "$ISABELLE_HOME/etc/settings"} file of the distribution).
   208   
   209   The actual compiler binary will be run from the directory @{setting
   210   ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
   211   command line.  The optional @{setting ML_PLATFORM} may specify the
   212   binary format of ML heap images, which is useful for cross-platform
   213   installations.  The value of @{setting ML_IDENTIFIER} is
   214   automatically obtained by composing the values of @{setting
   215   ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
   216 
   217   \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
   218   (Java Development Kit) installation with @{verbatim javac} and
   219   @{verbatim jar} executables.  This is essential for Isabelle/Scala
   220   and other JVM-based tools to work properly.  Note that conventional
   221   @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime
   222   Environment), not JDK.
   223   
   224   \item[@{setting_def ISABELLE_PATH}] is a list of directories
   225   (separated by colons) where Isabelle logic images may reside.  When
   226   looking up heaps files, the value of @{setting ML_IDENTIFIER} is
   227   appended to each component internally.
   228   
   229   \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
   230   directory where output heap files should be stored by default. The
   231   ML system and Isabelle version identifier is appended here, too.
   232   
   233   \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
   234   theory browser information (HTML text, graph data, and printable
   235   documents) is stored (see also \secref{sec:info}).  The default
   236   value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
   237   
   238   \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
   239   load if none is given explicitely by the user.  The default value is
   240   @{verbatim HOL}.
   241   
   242   \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
   243   line editor for the @{tool_ref tty} interface.
   244 
   245   \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
   246   to the command line of any @{tool_ref usedir} invocation. This
   247   typically contains compilation options for object-logics --- @{tool
   248   usedir} is the basic tool for managing logic sessions (cf.\ the
   249   @{verbatim IsaMakefile}s in the distribution).
   250 
   251   \item[@{setting_def ISABELLE_LATEX}, @{setting_def
   252   ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
   253   ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
   254   document preparation (see also \secref{sec:tool-latex}).
   255   
   256   \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
   257   directories that are scanned by @{executable isabelle} for external
   258   utility programs (see also \secref{sec:isabelle-tool}).
   259   
   260   \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
   261   directories with documentation files.
   262   
   263   \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
   264   document format, typically @{verbatim dvi} or @{verbatim pdf}.
   265   
   266   \item[@{setting_def DVI_VIEWER}] specifies the command to be used
   267   for displaying @{verbatim dvi} files.
   268   
   269   \item[@{setting_def PDF_VIEWER}] specifies the command to be used
   270   for displaying @{verbatim pdf} files.
   271   
   272   \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
   273   spool command, which is expected to accept @{verbatim ps} files.
   274   
   275   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
   276   prefix from which any running @{executable "isabelle-process"}
   277   derives an individual directory for temporary files.  The default is
   278   somewhere in @{verbatim "/tmp"}.
   279   
   280   \end{description}
   281 *}
   282 
   283 
   284 subsection {* Additional components \label{sec:components} *}
   285 
   286 text {* Any directory may be registered as an explicit \emph{Isabelle
   287   component}.  The general layout conventions are that of the main
   288   Isabelle distribution itself, and the following two files (both
   289   optional) have a special meaning:
   290 
   291   \begin{itemize}
   292 
   293   \item @{verbatim "etc/settings"} holds additional settings that are
   294   initialized when bootstrapping the overall Isabelle environment,
   295   cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
   296   @{verbatim bash} script.  It may refer to the component's enclosing
   297   directory via the @{verbatim "COMPONENT"} shell variable.
   298 
   299   For example, the following setting allows to refer to files within
   300   the component later on, without having to hardwire absolute paths:
   301 
   302 \begin{ttbox}
   303 MY_COMPONENT_HOME="$COMPONENT"
   304 \end{ttbox}
   305 
   306   Components can also add to existing Isabelle settings such as
   307   @{setting_def ISABELLE_TOOLS}, in order to provide
   308   component-specific tools that can be invoked by end-users.  For
   309   example:
   310 
   311 \begin{ttbox}
   312 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
   313 \end{ttbox}
   314 
   315   \item @{verbatim "etc/components"} holds a list of further
   316   sub-components of the same structure.  The directory specifications
   317   given here can be either absolute (with leading @{verbatim "/"}) or
   318   relative to the component's main directory.
   319 
   320   \end{itemize}
   321 
   322   The root of component initialization is @{setting ISABELLE_HOME}
   323   itself.  After initializing all of its sub-components recursively,
   324   @{setting ISABELLE_HOME_USER} is included in the same manner (if
   325   that directory exists).  This allows to install private components
   326   via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
   327   often more convenient to do that programmatically via the
   328   \verb,init_component, shell function in the \verb,etc/settings,
   329   script of \verb,$ISABELLE_HOME_USER, (or any other component
   330   directory).  For example:
   331 \begin{ttbox}
   332 init_component "$HOME/screwdriver-2.0"
   333 \end{ttbox}
   334 
   335   This is tolerant wrt.\ missing component directories, but might
   336   produce a warning.
   337 
   338   \medskip More complex situations may be addressed by initializing
   339   components listed in a given catalog file, relatively to some base
   340   directory:
   341 
   342 \begin{ttbox}
   343 init_components "$HOME/my_component_store" "some_catalog_file"
   344 \end{ttbox}
   345 
   346   The component directories listed in the catalog file are treated as
   347   relative to the given base directory.
   348 
   349   See also \secref{sec:tool-components} for some tool-support for
   350   resolving components that are formally initialized but not installed
   351   yet.
   352 *}
   353 
   354 
   355 section {* The raw Isabelle process *}
   356 
   357 text {*
   358   The @{executable_def "isabelle-process"} executable runs bare-bones
   359   Isabelle logic sessions --- either interactively or in batch mode.
   360   It provides an abstraction over the underlying ML system, and over
   361   the actual heap file locations.  Its usage is:
   362 
   363 \begin{ttbox}
   364 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
   365 
   366   Options are:
   367     -I           startup Isar interaction mode
   368     -P           startup Proof General interaction mode
   369     -S           secure mode -- disallow critical operations
   370     -T ADDR      startup process wrapper, with socket address
   371     -W IN:OUT    startup process wrapper, with input/output fifos
   372     -X           startup PGIP interaction mode
   373     -e MLTEXT    pass MLTEXT to the ML session
   374     -f           pass 'Session.finish();' to the ML session
   375     -m MODE      add print mode for output
   376     -q           non-interactive session
   377     -r           open heap file read-only
   378     -u           pass 'use"ROOT.ML";' to the ML session
   379     -w           reset write permissions on OUTPUT
   380 
   381   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
   382   These are either names to be searched in the Isabelle path, or
   383   actual file names (containing at least one /).
   384   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   385 \end{ttbox}
   386 
   387   Input files without path specifications are looked up in the
   388   @{setting ISABELLE_PATH} setting, which may consist of multiple
   389   components separated by colons --- these are tried in the given
   390   order with the value of @{setting ML_IDENTIFIER} appended
   391   internally.  In a similar way, base names are relative to the
   392   directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
   393   actual file locations may also be given by including at least one
   394   slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
   395   refer to the current directory).
   396 *}
   397 
   398 
   399 subsubsection {* Options *}
   400 
   401 text {*
   402   If the input heap file does not have write permission bits set, or
   403   the @{verbatim "-r"} option is given explicitely, then the session
   404   started will be read-only.  That is, the ML world cannot be
   405   committed back into the image file.  Otherwise, a writable session
   406   enables commits into either the input file, or into another output
   407   heap file (if that is given as the second argument on the command
   408   line).
   409 
   410   The read-write state of sessions is determined at startup only, it
   411   cannot be changed intermediately. Also note that heap images may
   412   require considerable amounts of disk space (approximately
   413   50--200~MB). Users are responsible for themselves to dispose their
   414   heap files when they are no longer needed.
   415 
   416   \medskip The @{verbatim "-w"} option makes the output heap file
   417   read-only after terminating.  Thus subsequent invocations cause the
   418   logic image to be read-only automatically.
   419 
   420   \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
   421   passed to the Isabelle session from the command line. Multiple
   422   @{verbatim "-e"}'s are evaluated in the given order. Strange things
   423   may happen when errorneous ML code is provided. Also make sure that
   424   the ML commands are terminated properly by semicolon.
   425 
   426   \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
   427   "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
   428   The @{verbatim "-f"} option passes ``@{verbatim
   429   "Session.finish();"}'', which is intended mainly for administrative
   430   purposes.
   431 
   432   \medskip The @{verbatim "-m"} option adds identifiers of print modes
   433   to be made active for this session. Typically, this is used by some
   434   user interface, e.g.\ to enable output of proper mathematical
   435   symbols.
   436 
   437   \medskip Isabelle normally enters an interactive top-level loop
   438   (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
   439   option inhibits interaction, thus providing a pure batch mode
   440   facility.
   441 
   442   \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
   443   interaction mode on startup, instead of the primitive ML top-level.
   444   The @{verbatim "-P"} option configures the top-level loop for
   445   interaction with the Proof General user interface, and the
   446   @{verbatim "-X"} option enables XML-based PGIP communication.
   447 
   448   \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
   449   Isabelle enter a special process wrapper for interaction via the
   450   Isabelle/Scala layer, see also @{file
   451   "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
   452   the ML and JVM process is private to the implementation.
   453 
   454   \medskip The @{verbatim "-S"} option makes the Isabelle process more
   455   secure by disabling some critical operations, notably runtime
   456   compilation and evaluation of ML source code.
   457 *}
   458 
   459 
   460 subsubsection {* Examples *}
   461 
   462 text {*
   463   Run an interactive session of the default object-logic (as specified
   464   by the @{setting ISABELLE_LOGIC} setting) like this:
   465 \begin{ttbox}
   466 isabelle-process
   467 \end{ttbox}
   468 
   469   Usually @{setting ISABELLE_LOGIC} refers to one of the standard
   470   logic images, which are read-only by default.  A writable session
   471   --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
   472   directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
   473   may be invoked as follows:
   474 \begin{ttbox}
   475 isabelle-process HOL Test
   476 \end{ttbox}
   477   Ending this session normally (e.g.\ by typing control-D) dumps the
   478   whole ML system state into @{verbatim Test} (be prepared for more
   479   than 100\,MB):
   480 
   481   The @{verbatim Test} session may be continued later (still in
   482   writable state) by:
   483 \begin{ttbox}
   484 isabelle-process Test
   485 \end{ttbox}
   486   A read-only @{verbatim Test} session may be started by:
   487 \begin{ttbox}
   488 isabelle-process -r Test
   489 \end{ttbox}
   490 
   491   \medskip Note that manual session management like this does
   492   \emph{not} provide proper setup for theory presentation.  This would
   493   require @{tool usedir}.
   494 
   495   \bigskip The next example demonstrates batch execution of Isabelle.
   496   We retrieve the @{verbatim Main} theory value from the theory loader
   497   within ML (observe the delicate quoting rules for the Bash shell
   498   vs.\ ML):
   499 \begin{ttbox}
   500 isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
   501 \end{ttbox}
   502   Note that the output text will be interspersed with additional junk
   503   messages by the ML runtime environment.  The @{verbatim "-W"} option
   504   allows to communicate with the Isabelle process via an external
   505   program in a more robust fashion.
   506 *}
   507 
   508 
   509 section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
   510 
   511 text {*
   512   All Isabelle related tools and interfaces are called via a common
   513   wrapper --- @{executable isabelle}:
   514 
   515 \begin{ttbox}
   516 Usage: isabelle TOOL [ARGS ...]
   517 
   518   Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   519 
   520 Available tools:
   521   \dots
   522 \end{ttbox}
   523 
   524   In principle, Isabelle tools are ordinary executable scripts that
   525   are run within the Isabelle settings environment, see
   526   \secref{sec:settings}.  The set of available tools is collected by
   527   @{executable isabelle} from the directories listed in the @{setting
   528   ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
   529   from the shell.  Neither should you add the tool directories to your
   530   shell's search path!
   531 *}
   532 
   533 
   534 subsubsection {* Examples *}
   535 
   536 text {* Show the list of available documentation of the Isabelle
   537   distribution:
   538 
   539 \begin{ttbox}
   540   isabelle doc
   541 \end{ttbox}
   542 
   543   View a certain document as follows:
   544 \begin{ttbox}
   545   isabelle doc system
   546 \end{ttbox}
   547 
   548   Query the Isabelle settings environment:
   549 \begin{ttbox}
   550   isabelle getenv ISABELLE_HOME_USER
   551 \end{ttbox}
   552 *}
   553 
   554 end