doc-src/Ref/introduction.tex
author wenzelm
Tue May 04 11:27:25 1999 +0200 (1999-05-04)
changeset 6571 971f238ef3ec
parent 6569 66c941ea1f01
child 6618 13293a7d4a57
permissions -rw-r--r--
tuned;
wenzelm@3200
     1
lcp@104
     2
%% $Id$
wenzelm@3108
     3
lcp@286
     4
\chapter{Basic Use of Isabelle}\index{sessions|(} 
wenzelm@3108
     5
The Reference Manual is a comprehensive description of Isabelle
wenzelm@3108
     6
proper, including all \ML{} commands, functions and packages.  It
wenzelm@3108
     7
really is intended for reference, perhaps for browsing, but not for
wenzelm@3108
     8
reading through.  It is not a tutorial, but assumes familiarity with
wenzelm@3108
     9
the basic logical concepts of Isabelle.
lcp@104
    10
lcp@286
    11
When you are looking for a way of performing some task, scan the Table of
lcp@286
    12
Contents for a relevant heading.  Functions are organized by their purpose,
lcp@286
    13
by their operands (subgoals, tactics, theorems), and by their usefulness.
lcp@286
    14
In each section, basic functions appear first, then advanced functions, and
lcp@322
    15
finally esoteric functions.  Use the Index when you are looking for the
lcp@322
    16
definition of a particular Isabelle function.
lcp@104
    17
wenzelm@6568
    18
A few examples are presented.  Many example files are distributed with
lcp@286
    19
Isabelle, however; please experiment interactively.
lcp@104
    20
lcp@104
    21
lcp@104
    22
\section{Basic interaction with Isabelle}
paulson@2225
    23
\index{starting up|bold}\nobreak
paulson@2225
    24
%
wenzelm@6568
    25
We assume that your local Isabelle administrator (this might be you!) has
wenzelm@6568
    26
already installed the Isabelle system together with appropriate object-logics
wenzelm@6568
    27
--- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
wenzelm@6568
    28
top-level directory of the distribution on how to do this.
wenzelm@3108
    29
wenzelm@3108
    30
\medskip Let $\langle isabellehome \rangle$ denote the location where
paulson@3485
    31
the distribution has been installed.  To run Isabelle from a the shell
wenzelm@4317
    32
prompt within an ordinary text terminal session, simply type
wenzelm@3108
    33
\begin{ttbox}
wenzelm@3108
    34
\({\langle}isabellehome{\rangle}\)/bin/isabelle
wenzelm@3108
    35
\end{ttbox}
wenzelm@6568
    36
This should start an interactive \ML{} session with the default object-logic
wenzelm@6568
    37
(usually {\HOL}) already pre-loaded.
wenzelm@3108
    38
wenzelm@6568
    39
Subsequently, we assume that the \texttt{isabelle} executable is determined
wenzelm@6568
    40
automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
wenzelm@6568
    41
  \rangle\)/bin} to your search path.\footnote{Depending on your installation,
wenzelm@6568
    42
  there might be also stand-alone binaries located in some global directory
wenzelm@6568
    43
  such as \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle
wenzelm@6568
    44
    isabellehome \rangle\)/bin/isabelle}, though!  See \texttt{isatool
wenzelm@6568
    45
    install} in \emph{The Isabelle System Manual} of how to do this properly.}
wenzelm@3108
    46
wenzelm@6571
    47
\medskip
wenzelm@6571
    48
wenzelm@6568
    49
The object-logic image to load may be also specified explicitly as an argument
wenzelm@6568
    50
to the {\tt isabelle} command, e.g.
wenzelm@3108
    51
\begin{ttbox}
wenzelm@3108
    52
isabelle FOL
wenzelm@3108
    53
\end{ttbox}
wenzelm@6568
    54
This should put you into the world of polymorphic first-order logic (assuming
wenzelm@6568
    55
that an image of {\FOL} has been pre-built).
paulson@2225
    56
wenzelm@6568
    57
\index{saving your session|bold} Isabelle provides no means of storing
wenzelm@6568
    58
theorems or internal proof objects on files.  Theorems are simply part of the
wenzelm@6568
    59
\ML{} state.  To save your work between sessions, you may dump the \ML{}
wenzelm@6568
    60
system state to a file.  This is done automatically when ending the session
wenzelm@6568
    61
normally (e.g.\ by typing control-D), provided that the image has been opened
wenzelm@6568
    62
\emph{writable} in the first place.  The standard object-logic images are
wenzelm@6568
    63
usually read-only, so you have to create a private working copy first.  For
wenzelm@6568
    64
example, the following shell command puts you into a writable Isabelle session
wenzelm@6568
    65
of name \texttt{Foo} that initially contains just plain \HOL:
wenzelm@3108
    66
\begin{ttbox}
wenzelm@6568
    67
isabelle HOL Foo
wenzelm@3108
    68
\end{ttbox}
wenzelm@3108
    69
Ending the \texttt{Foo} session with control-D will cause the complete
wenzelm@6568
    70
\ML-world to be saved somewhere in your home directory\footnote{The default
wenzelm@6568
    71
  location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
wenzelm@6568
    72
  local configuration.}.  Make sure there is enough space available! Then one
wenzelm@6568
    73
may later continue at exactly the same point by running
wenzelm@3108
    74
\begin{ttbox}
wenzelm@3108
    75
isabelle Foo  
wenzelm@3108
    76
\end{ttbox}
lcp@104
    77
wenzelm@6568
    78
\medskip Saving the {\ML} state is not enough.  Record, on a file, the
wenzelm@6568
    79
top-level commands that generate your theories and proofs.  Such a record
wenzelm@6568
    80
allows you to replay the proofs whenever required, for instance after making
wenzelm@6571
    81
minor changes to the axioms.  Ideally, these sources will be somewhat
wenzelm@6568
    82
intelligible to others as a formal description of your work.
wenzelm@3108
    83
wenzelm@6568
    84
It is good practice to put all source files that constitute a separate
wenzelm@6568
    85
Isabelle session into an individual directory, together with an {\ML} file
wenzelm@6568
    86
called \texttt{ROOT.ML} that contains appropriate commands to load all other
wenzelm@6568
    87
files required.  Running \texttt{isabelle} with option \texttt{-u}
wenzelm@6568
    88
automatically loads \texttt{ROOT.ML} on entering the session.  The
wenzelm@6571
    89
\texttt{isatool usedir} utility provides some more options to manage Isabelle
wenzelm@6568
    90
sessions, such as automatic generation of theory browsing information.
lcp@104
    91
wenzelm@6568
    92
\medskip More details about the \texttt{isabelle} and \texttt{isatool}
wenzelm@6568
    93
commands may be found in \emph{The Isabelle System Manual}.
wenzelm@6568
    94
wenzelm@6568
    95
\medskip There are more comfortable user interfaces than the bare-bones \ML{}
wenzelm@6568
    96
top-level run from a text terminal.  The \texttt{Isabelle} executable (note
wenzelm@6568
    97
the capital I) runs one such interface, depending on your local configuration.
wenzelm@6568
    98
Again, see \emph{The Isabelle System Manual} for more information.
lcp@104
    99
lcp@104
   100
lcp@104
   101
\section{Ending a session}
lcp@104
   102
\begin{ttbox} 
wenzelm@3108
   103
quit    : unit -> unit
wenzelm@3108
   104
exit    : int -> unit
wenzelm@6067
   105
commit  : unit -> bool
lcp@104
   106
\end{ttbox}
lcp@322
   107
\begin{ttdescription}
wenzelm@3108
   108
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
wenzelm@3108
   109
  the state.
wenzelm@4317
   110
  
wenzelm@4317
   111
\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
wenzelm@4317
   112
  code \(i\) to the operating system.
lcp@104
   113
wenzelm@3108
   114
\item[\ttindexbold{commit}();] saves the current state without ending
wenzelm@6067
   115
  the session, provided that the logic image is opened read-write;
wenzelm@6067
   116
  return value {\tt false} indicates an error.
lcp@322
   117
\end{ttdescription}
lcp@104
   118
wenzelm@3108
   119
Typing control-D also finishes the session in essentially the same way
wenzelm@3108
   120
as the sequence {\tt commit(); quit();} would.
lcp@104
   121
lcp@104
   122
lcp@322
   123
\section{Reading ML files}
lcp@322
   124
\index{files!reading}
lcp@104
   125
\begin{ttbox} 
clasohm@138
   126
cd              : string -> unit
clasohm@884
   127
pwd             : unit -> string
clasohm@138
   128
use             : string -> unit
clasohm@138
   129
time_use        : string -> unit
lcp@104
   130
\end{ttbox}
lcp@322
   131
\begin{ttdescription}
wenzelm@4317
   132
\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
wenzelm@4317
   133
  {\it dir}.  This is the default directory for reading files.
wenzelm@4317
   134
  
wenzelm@4317
   135
\item[\ttindexbold{pwd}();] returns the full path of the current
wenzelm@4317
   136
  directory.
clasohm@884
   137
lcp@322
   138
\item[\ttindexbold{use} "$file$";]  
lcp@104
   139
reads the given {\it file} as input to the \ML{} session.  Reading a file
lcp@104
   140
of Isabelle commands is the usual way of replaying a proof.
lcp@104
   141
lcp@322
   142
\item[\ttindexbold{time_use} "$file$";]  
lcp@104
   143
performs {\tt use~"$file$"} and prints the total execution time.
lcp@322
   144
\end{ttdescription}
lcp@104
   145
wenzelm@6343
   146
The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
wenzelm@6343
   147
commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
wenzelm@6343
   148
expanded appropriately.  Note that \texttt{\~\relax} abbreviates
wenzelm@6343
   149
\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
wenzelm@6571
   150
\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.  The syntax for path
wenzelm@6571
   151
specifications follows Unix conventions.
wenzelm@6568
   152
wenzelm@6568
   153
wenzelm@6568
   154
\section{Reading theories}\label{sec:intro-theories}
wenzelm@6568
   155
\index{theories!reading}
wenzelm@6568
   156
wenzelm@6568
   157
In Isabelle, any kind of declarations, definitions, etc.\ are organized around
wenzelm@6568
   158
named \emph{theory} objects.  Logical reasoning always takes place within a
wenzelm@6568
   159
certain theory context, which may be switched at any time.  Theory $name$ is
wenzelm@6568
   160
defined by a theory file $name$\texttt{.thy}, containing declarations of
wenzelm@6568
   161
\texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
wenzelm@6568
   162
\S\ref{sec:ref-defining-theories} for more details on concrete syntax).
wenzelm@6568
   163
Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
wenzelm@6568
   164
proof scripts that are to be run in the context of the theory.
wenzelm@6568
   165
wenzelm@6568
   166
\begin{ttbox}
wenzelm@6568
   167
context      : theory -> unit
wenzelm@6568
   168
the_context  : unit -> theory
wenzelm@6568
   169
theory       : string -> theory
wenzelm@6568
   170
use_thy      : string -> unit
wenzelm@6568
   171
time_use_thy : string -> unit
wenzelm@6568
   172
\end{ttbox}
wenzelm@6568
   173
wenzelm@6568
   174
\begin{ttdescription}
wenzelm@6568
   175
  
wenzelm@6568
   176
\item[\ttindexbold{context} $thy$;] switches the current theory context.  Any
wenzelm@6568
   177
  subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
wenzelm@6568
   178
  will refer to $thy$ as its theory.
wenzelm@6568
   179
  
wenzelm@6568
   180
\item[\ttindexbold{the_context}();] obtains the current theory context, or
wenzelm@6568
   181
  raises an error if absent.
wenzelm@6568
   182
  
wenzelm@6569
   183
\item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
wenzelm@6568
   184
  the internal database of loaded theories, raising an error if absent.
wenzelm@6568
   185
  
wenzelm@6569
   186
\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
wenzelm@6571
   187
  system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter
wenzelm@6571
   188
  being optional).  It also ensures that all parent theories are loaded as
wenzelm@6571
   189
  well.  In case some older versions have already been present,
wenzelm@6571
   190
  \texttt{use_thy} only tries to reload $name$ itself, but is content with any
wenzelm@6571
   191
  version of its ancestors.
wenzelm@6568
   192
  
wenzelm@6569
   193
\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
wenzelm@6568
   194
  reports the time taken to process the actual theory parts and {\ML} files
wenzelm@6568
   195
  separately.
wenzelm@6568
   196
  
wenzelm@6568
   197
\end{ttdescription}
wenzelm@6568
   198
wenzelm@6568
   199
See \S\ref{sec:more-theories} for further information on Isabelle's theory
wenzelm@6568
   200
loader.
wenzelm@4274
   201
lcp@104
   202
wenzelm@3108
   203
\section{Setting flags}
wenzelm@3108
   204
\begin{ttbox}
wenzelm@3108
   205
set     : bool ref -> bool
wenzelm@3108
   206
reset   : bool ref -> bool
wenzelm@3108
   207
toggle  : bool ref -> bool
wenzelm@3108
   208
\end{ttbox}\index{*set}\index{*reset}\index{*toggle}
paulson@3485
   209
These are some shorthands for manipulating boolean references.  The new
wenzelm@3108
   210
value is returned.
wenzelm@3108
   211
wenzelm@3108
   212
lcp@508
   213
\section{Printing of terms and theorems}\label{sec:printing-control}
lcp@322
   214
\index{printing control|(}
lcp@104
   215
Isabelle's pretty printer is controlled by a number of parameters.
lcp@104
   216
lcp@104
   217
\subsection{Printing limits}
lcp@104
   218
\begin{ttbox} 
lcp@104
   219
Pretty.setdepth  : int -> unit
lcp@104
   220
Pretty.setmargin : int -> unit
lcp@104
   221
print_depth      : int -> unit
lcp@104
   222
\end{ttbox}
wenzelm@4317
   223
These set limits for terminal output.  See also {\tt goals_limit},
wenzelm@4317
   224
which limits the number of subgoals printed
wenzelm@4317
   225
(\S\ref{sec:goals-printing}).
lcp@104
   226
lcp@322
   227
\begin{ttdescription}
wenzelm@6571
   228
\item[\ttindexbold{Pretty.setdepth} \(d\);] tells Isabelle's pretty printer to
wenzelm@6571
   229
  limit the printing depth to~$d$.  This affects the display of theorems and
wenzelm@6571
   230
  terms.  The default value is~0, which permits printing to an arbitrary
wenzelm@6571
   231
  depth.  Useful values for $d$ are~10 and~20.
lcp@104
   232
lcp@322
   233
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
lcp@322
   234
  tells Isabelle's pretty printer to assume a right margin (page width)
wenzelm@4317
   235
  of~$m$.  The initial margin is~76.
lcp@104
   236
lcp@322
   237
\item[\ttindexbold{print_depth} \(n\);]  
lcp@322
   238
  limits the printing depth of complex \ML{} values, such as theorems and
lcp@322
   239
  terms.  This command affects the \ML{} top level and its effect is
lcp@322
   240
  compiler-dependent.  Typically $n$ should be less than~10.
lcp@322
   241
\end{ttdescription}
lcp@104
   242
lcp@104
   243
wenzelm@4317
   244
\subsection{Printing of hypotheses, brackets, types etc.}
lcp@322
   245
\index{meta-assumptions!printing of}
lcp@322
   246
\index{types!printing of}\index{sorts!printing of}
lcp@104
   247
\begin{ttbox} 
lcp@508
   248
show_hyps     : bool ref \hfill{\bf initially true}
wenzelm@6343
   249
show_tags     : bool ref \hfill{\bf initially false}
lcp@508
   250
show_brackets : bool ref \hfill{\bf initially false}
lcp@508
   251
show_types    : bool ref \hfill{\bf initially false}
lcp@508
   252
show_sorts    : bool ref \hfill{\bf initially false}
wenzelm@4317
   253
show_consts   : bool ref \hfill{\bf initially false}
wenzelm@4543
   254
long_names    : bool ref \hfill{\bf initially false}
lcp@104
   255
\end{ttbox}
lcp@322
   256
These flags allow you to control how much information is displayed for
wenzelm@4317
   257
types, terms and theorems.  The hypotheses of theorems \emph{are}
wenzelm@4317
   258
normally shown.  Superfluous parentheses of types and terms are not.
wenzelm@4317
   259
Types and sorts of variables are normally hidden.
wenzelm@4317
   260
wenzelm@4317
   261
Note that displaying types and sorts may explain why a polymorphic
wenzelm@4317
   262
inference rule fails to resolve with some goal, or why a rewrite rule
wenzelm@4317
   263
does not apply as expected.
lcp@104
   264
lcp@322
   265
\begin{ttdescription}
wenzelm@4543
   266
wenzelm@4317
   267
\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
wenzelm@4317
   268
  meta-level hypothesis as a dot.
wenzelm@4317
   269
  
wenzelm@6343
   270
\item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
wenzelm@6343
   271
  (which are basically just comments that may be attached by some tools).
wenzelm@6343
   272
  
wenzelm@4317
   273
\item[set \ttindexbold{show_brackets};] makes Isabelle show full
wenzelm@4317
   274
  bracketing.  In particular, this reveals the grouping of infix
wenzelm@4317
   275
  operators.
wenzelm@4317
   276
  
wenzelm@4317
   277
\item[set \ttindexbold{show_types};] makes Isabelle show types when
wenzelm@4317
   278
  printing a term or theorem.
wenzelm@4317
   279
  
wenzelm@4317
   280
\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
wenzelm@4317
   281
  and the sorts of type variables, independently of the value of
wenzelm@4317
   282
  \texttt{show_types}.
wenzelm@4543
   283
wenzelm@4317
   284
\item[set \ttindexbold{show_consts};] makes Isabelle show types of
wenzelm@4317
   285
  constants, provided that showing of types is enabled at all.  This
wenzelm@4317
   286
  is supported for printing of proof states only.  Note that the
wenzelm@4317
   287
  output can be enormous as polymorphic constants often occur at
wenzelm@4317
   288
  several different type instances.
lcp@508
   289
wenzelm@4543
   290
\item[set \ttindexbold{long_names};] forces names of all objects
wenzelm@4543
   291
  (types, constants, theorems, etc.) to be printed in their fully
wenzelm@4543
   292
  qualified internal form.
wenzelm@4543
   293
lcp@322
   294
\end{ttdescription}
lcp@104
   295
lcp@104
   296
lcp@104
   297
\subsection{$\eta$-contraction before printing}
lcp@104
   298
\begin{ttbox} 
lcp@104
   299
eta_contract: bool ref \hfill{\bf initially false}
lcp@104
   300
\end{ttbox}
lcp@104
   301
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
lcp@104
   302
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
lcp@104
   303
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
lcp@332
   304
unification frequently puts terms into a fully $\eta$-expanded form.  For
lcp@158
   305
example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
lcp@158
   306
$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
lcp@158
   307
form.
lcp@104
   308
lcp@322
   309
\begin{ttdescription}
wenzelm@4317
   310
\item[set \ttindexbold{eta_contract};]
lcp@104
   311
makes Isabelle perform $\eta$-contractions before printing, so that
lcp@104
   312
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
lcp@104
   313
distinction between a term and its $\eta$-expanded form occasionally
lcp@104
   314
matters.
lcp@322
   315
\end{ttdescription}
lcp@322
   316
\index{printing control|)}
lcp@104
   317
wenzelm@4317
   318
\section{Diagnostic messages}
wenzelm@4317
   319
\index{error messages}
wenzelm@4317
   320
\index{warnings}
wenzelm@4317
   321
wenzelm@6568
   322
Isabelle conceptually provides three output channels for different kinds of
wenzelm@6568
   323
messages: ordinary text, warnings, errors.  Depending on the user interface
wenzelm@6568
   324
involved, these messages may appear in different text styles or colours.
wenzelm@4317
   325
wenzelm@4317
   326
The default setup of an \texttt{isabelle} terminal session is as
wenzelm@4317
   327
follows: plain output of ordinary text, warnings prefixed by
wenzelm@4317
   328
\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
wenzelm@4317
   329
typical warning would look like this:
wenzelm@4317
   330
\begin{ttbox}
wenzelm@4317
   331
\#\#\# Beware the Jabberwock, my son!
wenzelm@4317
   332
\#\#\# The jaws that bite, the claws that catch!
wenzelm@4317
   333
\#\#\# Beware the Jubjub Bird, and shun
wenzelm@4317
   334
\#\#\# The frumious Bandersnatch!
wenzelm@4317
   335
\end{ttbox}
wenzelm@4317
   336
wenzelm@4317
   337
\texttt{ML} programs may output diagnostic messages using the
wenzelm@4317
   338
following functions:
wenzelm@4317
   339
\begin{ttbox}
wenzelm@4317
   340
writeln : string -> unit
wenzelm@4317
   341
warning : string -> unit
wenzelm@4317
   342
error   : string -> 'a
wenzelm@4317
   343
\end{ttbox}
wenzelm@4317
   344
Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
wenzelm@4317
   345
after having output the text, while \ttindex{writeln} and
wenzelm@4317
   346
\ttindex{warning} resume normal program execution.
wenzelm@4317
   347
lcp@104
   348
lcp@104
   349
\section{Displaying exceptions as error messages}
lcp@322
   350
\index{exceptions!printing of}
lcp@104
   351
\begin{ttbox} 
lcp@104
   352
print_exn: exn -> 'a
lcp@104
   353
\end{ttbox}
lcp@104
   354
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
lcp@104
   355
and {\tt RSN}, are called both interactively and from programs.  They
lcp@104
   356
indicate errors not by printing messages, but by raising exceptions.  For
wenzelm@4317
   357
interactive use, \ML's reporting of an uncaught exception may be
lcp@322
   358
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
lcp@322
   359
backtrace.\index{Poly/{\ML} compiler}
lcp@104
   360
lcp@322
   361
\begin{ttdescription}
lcp@104
   362
\item[\ttindexbold{print_exn} $e$] 
lcp@104
   363
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
lcp@322
   364
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
lcp@322
   365
$EXP$ is an expression that may raise an exception.
lcp@104
   366
lcp@104
   367
{\tt print_exn} can display the following common exceptions, which concern
lcp@104
   368
types, terms, theorems and theories, respectively.  Each carries a message
lcp@104
   369
and related information.
lcp@104
   370
\begin{ttbox} 
lcp@104
   371
exception TYPE   of string * typ list * term list
lcp@104
   372
exception TERM   of string * term list
lcp@104
   373
exception THM    of string * int * thm list
lcp@104
   374
exception THEORY of string * theory list
lcp@104
   375
\end{ttbox}
lcp@322
   376
\end{ttdescription}
lcp@322
   377
\begin{warn}
lcp@322
   378
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
lcp@322
   379
  pretty printing information from the proof state last stored in the
lcp@322
   380
  subgoal module.  The appearance of the output thus depends upon the
lcp@322
   381
  theory used in the last interactive proof.
lcp@322
   382
\end{warn}
lcp@104
   383
lcp@104
   384
\index{sessions|)}
wenzelm@5371
   385
wenzelm@5371
   386
wenzelm@5371
   387
%%% Local Variables: 
wenzelm@5371
   388
%%% mode: latex
wenzelm@5371
   389
%%% TeX-master: "ref"
wenzelm@5371
   390
%%% End: