doc-src/System/Thy/Basics.thy
author wenzelm
Mon, 15 Sep 2008 16:42:00 +0200
changeset 28215 a1cfc43ac47d
child 28223 eee194395fdc
permissions -rw-r--r--
converted basics.tex to theory file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     1
(* $Id$ *)
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     2
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     3
theory Basics
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     4
imports Pure
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     5
begin
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     6
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     7
chapter {* The Isabelle system environment *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     8
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     9
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    10
  This manual describes Isabelle together with related tools and user
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    11
  interfaces as seen from an outside (system oriented) view.  See also
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    12
  the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    13
  and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    14
  actual Isabelle commands and related functions.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    15
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    16
  \medskip The Isabelle system environment emerges from a few general
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    17
  concepts.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    18
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    19
  \begin{itemize}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    20
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    21
  \item The \emph{Isabelle settings mechanism} provides environment variables to
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    22
  all Isabelle programs (including tools and user interfaces).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    23
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    24
  \item The \emph{Isabelle tools wrapper} (@{executable_def isatool})
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    25
  provides a generic startup platform for Isabelle related utilities.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    26
  Thus tools automatically benefit from the settings mechanism.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    27
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    28
  \item The raw \emph{Isabelle process} (@{executable_def isabelle} or
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    29
  @{executable_def "isabelle-process"}) runs logic sessions either
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    30
  interactively or in batch mode.  In particular, this view abstracts
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    31
  over the invocation of the actual ML system to be used.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    32
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    33
  \item The \emph{Isabelle interface wrapper} (@{executable_def
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    34
  Isabelle} or @{executable_def "isabelle-interface"}) provides some
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    35
  abstraction over the actual user interface to be used.  The de-facto
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    36
  standard interface for Isabelle is Proof~General
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    37
  \cite{proofgeneral}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    38
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    39
  \end{itemize}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    40
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    41
  \medskip The beginning user would probably just run the default user
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    42
  interface (by invoking the capital @{executable Isabelle}).  This
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    43
  assumes that the system has already been installed, of course.  In
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    44
  case you have to do this yourself, see the @{verbatim INSTALL} file
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    45
  in the top-level directory of the distribution of how to proceed;
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    46
  binary packages for various system components are available as well.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    47
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    48
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    49
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    50
section {* Isabelle settings \label{sec:settings} *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    51
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    52
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    53
  The Isabelle system heavily depends on the \emph{settings
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    54
  mechanism}\indexbold{settings}.  Essentially, this is a statically
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    55
  scoped collection of environment variables, such as @{setting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    56
  ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    57
  variables are \emph{not} intended to be set directly from the shell,
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    58
  though.  Isabelle employs a somewhat more sophisticated scheme of
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    59
  \emph{settings files} --- one for site-wide defaults, another for
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    60
  additional user-specific modifications.  With all configuration
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    61
  variables in at most two places, this scheme is more maintainable
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    62
  and user-friendly than global shell environment variables.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    63
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    64
  In particular, we avoid the typical situation where prospective
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    65
  users of a software package are told to put several things into
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    66
  their shell startup scripts, before being able to actually run the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    67
  program. Isabelle requires none such administrative chores of its
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    68
  end-users --- the executables can be invoked straight away.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    69
  Occasionally, users would still want to put the Isabelle @{verbatim
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    70
  bin} directory into their shell's search path, but this is not
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    71
  required.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    72
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    73
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    74
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    75
subsection {* Building the environment *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    76
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    77
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    78
  Whenever any of the Isabelle executables is run, their settings
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    79
  environment is put together as follows.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    80
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    81
  \begin{enumerate}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    82
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    83
  \item The special variable @{setting_def ISABELLE_HOME} is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    84
  determined automatically from the location of the binary that has
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    85
  been run.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    86
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    87
  You should not try to set @{setting ISABELLE_HOME} manually. Also
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    88
  note that the Isabelle executables either have to be run from their
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    89
  original location in the distribution directory, or via the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    90
  executable objects created by the @{tool install} utility (see
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    91
  \secref{sec:tool-install}).  Just doing a plain copy of the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    92
  @{verbatim bin} files will not work!
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    93
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    94
  \item The file @{verbatim "$ISABELLE_HOME/etc/settings"} ist run as
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    95
  a shell script with the auto-export option for variables enabled.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    96
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    97
  This file holds a rather long list of shell variable assigments,
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    98
  thus providing the site-wide default settings.  The Isabelle
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    99
  distribution already contains a global settings file with sensible
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   100
  defaults for most variables.  When installing the system, only a few
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   101
  of these may have to be adapted (probably @{setting ML_SYSTEM}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   102
  etc.).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   103
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   104
  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   105
  exists) is run in the same way as the site default settings. Note
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   106
  that the variable @{setting ISABELLE_HOME_USER} has already been set
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   107
  before --- usually to @{verbatim "~/isabelle"}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   108
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   109
  Thus individual users may override the site-wide defaults.  See also
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   110
  file @{verbatim "etc/user-settings.sample"} in the distribution.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   111
  Typically, a user settings file would contain only a few lines, just
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   112
  the assigments that are really changed.  One should definitely
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   113
  \emph{not} start with a full copy the basic @{verbatim
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   114
  "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   115
  maintainance problems later, when the Isabelle installation is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   116
  updated or changed otherwise.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   117
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   118
  \end{enumerate}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   119
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   120
  Note that settings files are actually full GNU bash scripts. So one
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   121
  may use complex shell commands, such as @{verbatim "if"} or
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   122
  @{verbatim "case"} statements to set variables depending on the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   123
  system architecture or other environment variables.  Such advanced
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   124
  features should be added only with great care, though. In
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   125
  particular, external environment references should be kept at a
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   126
  minimum.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   127
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   128
  \medskip A few variables are somewhat special:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   129
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   130
  \begin{itemize}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   131
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   132
  \item @{setting_def ISABELLE} and @{setting_def ISATOOL} are set
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   133
  automatically to the absolute path names of the @{executable
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   134
  "isabelle-process"} and @{executable isatool} executables,
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   135
  respectively.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   136
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   137
  \item @{setting_def ISABELLE_OUTPUT} will have the identifiers of
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   138
  the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   139
  the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   140
  to its value.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   141
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   142
  \end{itemize}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   143
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   144
  \medskip The Isabelle settings scheme is conceptually simple, but
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   145
  not completely trivial.  For debugging purposes, the resulting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   146
  environment may be inspected with the @{tool getenv} utility, see
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   147
  \secref{sec:tool-getenv}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   148
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   149
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   150
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   151
subsection{* Common variables *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   152
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   153
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   154
  This is a reference of common Isabelle settings variables. Note that
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   155
  the list is somewhat open-ended. Third-party utilities or interfaces
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   156
  may add their own selection. Variables that are special in some
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   157
  sense are marked with @{text "\<^sup>*"}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   158
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   159
  \begin{description}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   160
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   161
  \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   162
  location of the top-level Isabelle distribution directory. This is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   163
  automatically determined from the Isabelle executable that has been
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   164
  invoked.  Do not attempt to set @{setting ISABELLE_HOME} yourself
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   165
  from the shell.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   166
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   167
  \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   168
  counterpart of @{setting ISABELLE_HOME}. The default value is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   169
  @{verbatim "~/isabelle"}, under rare circumstances this may be
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   170
  changed in the global setting file.  Typically, the @{setting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   171
  ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   172
  some extend. In particular, site-wide defaults may be overridden by
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   173
  a private @{verbatim "etc/settings"}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   174
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   175
  \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   176
  ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   177
  names of the @{executable "isabelle-process"} and @{executable
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   178
  isatool} executables, respectively.  Thus other tools and scripts
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   179
  need not assume that the Isabelle @{verbatim bin} directory is on
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   180
  the current search path of the shell.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   181
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   182
  \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   183
  to the name of this Isabelle distribution, e.g.\ ``@{verbatim
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   184
  Isabelle2008}''.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   185
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   186
  \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   187
  @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   188
  ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   189
  to be used for Isabelle.  There is only a fixed set of admissable
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   190
  @{setting ML_SYSTEM} names (see the @{verbatim "etc/settings"} file
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   191
  of the distribution).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   192
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   193
  The actual compiler binary will be run from the directory @{setting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   194
  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   195
  command line.  The optional @{setting ML_PLATFORM} may specify the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   196
  binary format of ML heap images, which is useful for cross-platform
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   197
  installations.  The value of @{setting ML_IDENTIFIER} is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   198
  automatically obtained by composing the values of @{setting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   199
  ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   200
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   201
  \item[@{setting_def ISABELLE_PATH}] is a list of directories
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   202
  (separated by colons) where Isabelle logic images may reside.  When
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   203
  looking up heaps files, the value of @{setting ML_IDENTIFIER} is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   204
  appended to each component internally.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   205
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   206
  \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   207
  directory where output heap files should be stored by default. The
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   208
  ML system and Isabelle version identifier is appended here, too.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   209
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   210
  \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   211
  theory browser information (HTML text, graph data, and printable
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   212
  documents) is stored (see also \secref{sec:info}).  The default
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   213
  value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   214
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   215
  \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   216
  load if none is given explicitely by the user.  The default value is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   217
  @{verbatim HOL}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   218
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   219
  \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   220
  line editor for @{verbatim "isatool tty"} (see also
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   221
  \secref{sec:tool-tty}).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   222
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   223
  \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   224
  to the command line of any @{verbatim "isatool usedir"} invocation
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   225
  (see also \secref{sec:tool-usedir}). This typically contains
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   226
  compilation options for object-logics --- @{tool usedir} is the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   227
  basic utility for managing logic sessions (cf.\ the @{verbatim
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   228
  IsaMakefile}s in the distribution).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   229
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   230
  \item[@{setting_def ISABELLE_FILE_IDENT}] specifies a shell command
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   231
  for producing a source file identification, based on the actual
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   232
  content instead of the full physical path and date stamp (which is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   233
  the default). A typical identification would produce a ``digest'' of
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   234
  the text, using a cryptographic hash function like SHA-1, for
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   235
  example.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   236
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   237
  \item[@{setting_def ISABELLE_LATEX}, @{setting_def
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   238
  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   239
  ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   240
  document preparation (see also \secref{sec:tool-latex}).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   241
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   242
  \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   243
  directories that are scanned by @{executable isatool} for external
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   244
  utility programs (see also \secref{sec:isatool}).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   245
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   246
  \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   247
  directories with documentation files.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   248
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   249
  \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   250
  document format, typically @{verbatim dvi} or @{verbatim pdf}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   251
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   252
  \item[@{setting_def DVI_VIEWER}] specifies the command to be used
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   253
  for displaying @{verbatim dvi} files.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   254
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   255
  \item[@{setting_def PDF_VIEWER}] specifies the command to be used
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   256
  for displaying @{verbatim pdf} files.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   257
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   258
  \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   259
  spool command, which is expected to accept @{verbatim ps} files.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   260
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   261
  \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   262
  prefix from which any running @{executable isabelle} process derives
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   263
  an individual directory for temporary files.  The default is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   264
  somewhere in @{verbatim "/tmp"}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   265
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   266
  \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   267
  specifies the actual user interface that the capital @{executable
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   268
  Isabelle} or @{executable "isabelle-interface"} should invoke.  See
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   269
  \secref{sec:interface} for more details.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   270
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   271
  \end{description}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   272
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   273
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   274
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   275
section {* The Isabelle tools wrapper \label{sec:isatool} *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   276
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   277
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   278
  All Isabelle related utilities are called via a common wrapper ---
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   279
  \ttindex{isatool}:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   280
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   281
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   282
Usage: isatool TOOL [ARGS ...]
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   283
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   284
  Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   285
  for more specific help.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   286
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   287
  Available tools are:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   288
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   289
    browser - Isabelle graph browser
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   290
    \dots
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   291
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   292
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   293
  In principle, Isabelle tools are ordinary executable scripts that
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   294
  are run within the Isabelle settings environment, see
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   295
  \secref{sec:settings}.  The set of available tools is collected by
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   296
  @{executable isatool} from the directories listed in the @{setting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   297
  ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   298
  from the shell.  Neither should you add the tool directories to your
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   299
  shell's search path!
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   300
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   301
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   302
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   303
subsubsection {* Examples *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   304
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   305
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   306
  Show the list of available documentation of the current Isabelle
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   307
  installation like this:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   308
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   309
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   310
  isatool doc
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   311
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   312
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   313
  View a certain document as follows:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   314
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   315
  isatool doc isar-ref
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   316
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   317
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   318
  Create an Isabelle session derived from HOL (see also
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   319
  \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   320
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   321
  isatool mkdir HOL Test && isatool make
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   322
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   323
  Note that @{verbatim "isatool mkdir"} is usually only invoked once;
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   324
  existing sessions (including document output etc.) are then updated
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   325
  by @{verbatim "isatool make"} alone.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   326
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   327
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   328
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   329
section {* The raw Isabelle process *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   330
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   331
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   332
  The @{executable_ref isabelle} (or @{executable_ref
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   333
  "isabelle-process"}) executable runs bare-bones Isabelle logic
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   334
  sessions --- either interactively or in batch mode.  It provides an
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   335
  abstraction over the underlying ML system, and over the actual heap
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   336
  file locations.  Its usage is:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   337
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   338
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   339
Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   340
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   341
  Options are:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   342
    -C           tell ML system to copy output image
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   343
    -I           startup Isar interaction mode
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   344
    -P           startup Proof General interaction mode
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   345
    -S           secure mode -- disallow critical operations
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   346
    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   347
    -X           startup PGIP interaction mode
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   348
    -c           tell ML system to compress output image
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   349
    -e MLTEXT    pass MLTEXT to the ML session
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   350
    -f           pass 'Session.finish();' to the ML session
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   351
    -m MODE      add print mode for output
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   352
    -q           non-interactive session
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   353
    -r           open heap file read-only
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   354
    -u           pass 'use"ROOT.ML";' to the ML session
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   355
    -w           reset write permissions on OUTPUT
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   356
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   357
  INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   358
  These are either names to be searched in the Isabelle path, or
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   359
  actual file names (containing at least one /).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   360
  If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   361
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   362
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   363
  Input files without path specifications are looked up in the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   364
  @{setting ISABELLE_PATH} setting, which may consist of multiple
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   365
  components separated by colons --- these are tried in the given
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   366
  order with the value of @{setting ML_IDENTIFIER} appended
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   367
  internally.  In a similar way, base names are relative to the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   368
  directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   369
  actual file locations may also be given by including at least one
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   370
  slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   371
  refer to the current directory).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   372
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   373
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   374
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   375
subsection {* Options *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   376
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   377
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   378
  If the input heap file does not have write permission bits set, or
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   379
  the @{verbatim "-r"} option is given explicitely, then the session
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   380
  started will be read-only.  That is, the ML world cannot be
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   381
  committed back into the image file.  Otherwise, a writable session
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   382
  enables commits into either the input file, or into another output
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   383
  heap file (if that is given as the second argument on the command
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   384
  line).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   385
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   386
  The read-write state of sessions is determined at startup only, it
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   387
  cannot be changed intermediately. Also note that heap images may
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   388
  require considerable amounts of disk space (approximately
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   389
  50--200~MB). Users are responsible for themselves to dispose their
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   390
  heap files when they are no longer needed.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   391
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   392
  \medskip The @{verbatim "-w"} option makes the output heap file
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   393
  read-only after terminating.  Thus subsequent invocations cause the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   394
  logic image to be read-only automatically.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   395
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   396
  \medskip The @{verbatim "-c"} option tells the underlying ML system
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   397
  to compress the output heap (fully transparently).  On Poly/ML for
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   398
  example, the image is garbage collected and all stored values are
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   399
  maximally shared, resulting in up to @{text "50%"} less disk space
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   400
  consumption.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   401
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   402
  \medskip The @{verbatim "-C"} option tells the ML system to produce
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   403
  a completely self-contained output image, probably including a copy
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   404
  of the ML runtime system itself.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   405
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   406
  \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   407
  passed to the Isabelle session from the command line. Multiple
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   408
  @{verbatim "-e"}'s are evaluated in the given order. Strange things
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   409
  may happen when errorneous ML code is provided. Also make sure that
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   410
  the ML commands are terminated properly by semicolon.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   411
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   412
  \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   413
  "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   414
  The @{verbatim "-f"} option passes ``@{verbatim "Session.finish ();"}'',
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   415
  which is intended mainly for administrative purposes.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   416
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   417
  \medskip The @{verbatim "-m"} option adds identifiers of print modes
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   418
  to be made active for this session. Typically, this is used by some
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   419
  user interface, e.g.\ to enable output of proper mathematical
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   420
  symbols.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   421
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   422
  \medskip Isabelle normally enters an interactive top-level loop
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   423
  (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   424
  option inhibits interaction, thus providing a pure batch mode
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   425
  facility.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   426
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   427
  \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   428
  interaction mode on startup, instead of the primitive ML top-level.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   429
  The @{verbatim "-P"} option configures the top-level loop for
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   430
  interaction with the Proof General user interface, and the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   431
  @{verbatim "-X"} option enables XML-based PGIP communication.  The
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   432
  @{verbatim "-W"} option makes Isabelle enter a special process
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   433
  wrapper for interaction via an external program; the protocol is a
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   434
  stripped-down version of Proof General the interaction mode.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   435
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   436
  \medskip The @{verbatim "-S"} option makes the Isabelle process more
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   437
  secure by disabling some critical operations, notably runtime
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   438
  compilation and evaluation of ML source code.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   439
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   440
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   441
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   442
subsection {* Examples *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   443
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   444
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   445
  Run an interactive session of the default object-logic (as specified
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   446
  by the @{setting ISABELLE_LOGIC} setting) like this:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   447
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   448
isabelle
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   449
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   450
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   451
  Usually @{setting ISABELLE_LOGIC} refers to one of the standard
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   452
  logic images, which are read-only by default.  A writable session
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   453
  --- based on @{verbatim FOL}, but output to @{verbatim Foo} (in the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   454
  directory specified by the @{verbatim ISABELLE_OUTPUT} setting) ---
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   455
  may be invoked as follows:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   456
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   457
isabelle FOL Foo
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   458
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   459
  Ending this session normally (e.g.\ by typing control-D) dumps the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   460
  whole ML system state into @{verbatim Foo}. Be prepared for several
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   461
  tens of megabytes.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   462
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   463
  The @{verbatim Foo} session may be continued later (still in
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   464
  writable state) by:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   465
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   466
isabelle Foo
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   467
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   468
  A read-only @{verbatim Foo} session may be started by:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   469
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   470
isabelle -r Foo
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   471
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   472
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   473
  \medskip Note that manual session management like this does
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   474
  \emph{not} provide proper setup for theory presentation.  This would
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   475
  require the @{tool usedir} utility, see \secref{sec:tool-usedir}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   476
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   477
  \bigskip The next example demonstrates batch execution of
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   478
  Isabelle. We print a certain theorem of @{verbatim FOL}:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   479
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   480
isabelle -e "prth allE;" -q -r FOL
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   481
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   482
  Note that the output text will be interspersed with additional junk
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   483
  messages by the ML runtime environment.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   484
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   485
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   486
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   487
section {* The Isabelle interface wrapper \label{sec:interface} *}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   488
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   489
text {*
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   490
  Isabelle is a generic theorem prover, even w.r.t.\ its user
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   491
  interface.  The @{executable_ref Isabelle} (or @{executable_ref
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   492
  "isabelle-interface"}) executable provides a uniform way for
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   493
  end-users to invoke a certain interface; which one to start is
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   494
  determined by the @{setting_ref ISABELLE_INTERFACE} setting
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   495
  variable, which should give a full path specification to the actual
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   496
  executable.  Also note that the @{tool install} utility provides
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   497
  some options to install desktop environment icons (see
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   498
  \secref{sec:tool-install}).
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   499
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   500
  Presently, the most prominent Isabelle interface is Proof
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   501
  General~\cite{proofgeneral}\index{user interface!Proof General}.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   502
  The Proof General distribution includes an interface wrapper script
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   503
  for the regular Isar toplevel, see @{verbatim
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   504
  "ProofGeneral/isar/interface"}.  The canonical settings for
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   505
  Isabelle/Isar are as follows:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   506
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   507
\begin{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   508
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   509
PROOFGENERAL_OPTIONS=""
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   510
\end{ttbox}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   511
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   512
  Thus @{executable Isabelle} would automatically invoke Emacs with
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   513
  proper setup of the Proof General Lisp packages.  There are some
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   514
  options available, such as @{verbatim "-l"} for passing the logic
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   515
  image to be used by default, or @{verbatim "-m"} to tune the
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   516
  standard print mode.  The @{verbatim "-I"} option allows to switch
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   517
  between the Isar and ML view, independently of the interface script
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   518
  being used.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   519
  
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   520
  \medskip Note that the world may be also seen the other way round:
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   521
  Emacs may be started first (with proper setup of Proof General
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   522
  mode), and @{executable isabelle} run from within.  This requires
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   523
  further Emacs Lisp configuration, see the Proof General
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   524
  documentation \cite{proofgeneral} for more information.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   525
*}
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   526
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   527
end