# HG changeset patch
# User wenzelm
# Date 880655942 -3600
# Node ID 7264fa2ff2ec89a1ccf2eb0406f46518260b27f6
# Parent  86ac9153e6603a9f4e9ca8a3a504e7a952e4d9e3
several minor updates;

diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/classical.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -446,7 +446,7 @@
   proof using \texttt{blast_tac} can be made much faster by supplying the
   successful search bound to this tactic instead.
   
-\item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover}
+\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
   causes the tableau prover to print a trace of its search.  At each step it
   displays the formula currently being examined and reports whether the branch
   has been closed, extended or split.
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/goals.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -129,10 +129,10 @@
 store_thm : string * thm -> thm
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{qed} $name$] is the usual way of ending a proof.
-  It combines {\tt result} and {\tt bind_thm}: it gets the theorem using {\tt
-  result()} and stores it in Isabelle's theorem database.  See below for
-  details. 
+\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof.
+  It combines {\tt result} and {\tt bind_thm}: it gets the theorem
+  using {\tt result()} and stores it the theorem database associated
+  with its theory.  See below for details.
 
 \item[\ttindexbold{result}()]\index{assumptions!of main goal}
   returns the final theorem, after converting the free variables to
@@ -155,30 +155,32 @@
   definitions are unfolded in the main goal (by calling
   \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
   \ttindex{assume_ax} has been used.
-
-\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing}
+  
+\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
   stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
-  in Isabelle's theorem database and in the {\ML} variable $name$.  The
-  theorem can be retrieved from the database using {\tt get_thm}
-  (see \S\ref{BasicOperationsOnTheories}).
-
-\item[\ttindexbold{store_thm}($name$, $thm$)]\index{theorems!storing} stores
-  $thm$ in Isabelle's theorem database and returns that theorem.
+  in the theorem database associated with its theory and in the {\ML}
+  variable $name$.  The theorem can be retrieved from the database
+  using {\tt get_thm} (see \S\ref{BasicOperationsOnTheories}).
+  
+\item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing}
+  stores $thm$ in the theorem database associated with its theory and
+  returns that theorem.
 \end{ttdescription}
 
 
 \subsection{Retrieving theorems}
 \index{theorems!retrieving}
 
-The following functions retrieve theorems (together with their names) from
-the theorem database.  Hence they can only find theorems that have explicitly
-been stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
+The following functions retrieve theorems (together with their names)
+from the theorem database that is associated with the current proof
+state's theory.  They can only find theorems that have explicitly been
+stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
 related functions.
 \begin{ttbox} 
-findI           :         int -> (string * thm) list
-findE           :  int -> int -> (string * thm) list
-findEs          :         int -> (string * thm) list
-thms_containing : string list -> (string * thm) list
+findI           :          int -> (string * thm) list
+findE           :   int -> int -> (string * thm) list
+findEs          :          int -> (string * thm) list
+thms_containing : xstring list -> (string * thm) list
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
@@ -195,10 +197,10 @@
   to subgoal $i$ --- all those theorems whose first premise matches some
   premise of subgoal $i$.  Useful in connection with {\tt eresolve_tac} and
   {\tt dresolve_tac}.
-
-\item[\ttindexbold{thms_containing} $strings$] returns all theorems that
-  contain all of the constants in $strings$.  Note that a few basic constants
-  like \verb$==>$ are ignored.
+  
+\item[\ttindexbold{thms_containing} $consts$] returns all theorems
+  that contain all of a given set of constants.  Note that a few basic
+  constants like \verb$==>$ are ignored.
 \end{ttdescription}
 
 
@@ -282,7 +284,7 @@
 \end{ttbox}
 
 \begin{ttdescription}
-\item[\ttindexbold{proof_timing} := true;] 
+\item[set \ttindexbold{proof_timing};] 
 makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
 processor time was spent.  This information is compiler-dependent.
 \end{ttdescription}
@@ -375,11 +377,11 @@
 ren : string -> int -> unit
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{bw} {\it def};] 
-performs \hbox{\tt by (rewrite_goals_tac [{\it def}]);}
-It unfolds definitions in the subgoals (but not the main goal), by
-meta-rewriting with the given definition.
-\index{meta-rewriting}
+\item[\ttindexbold{bw} {\it def};] performs \hbox{\tt by
+    (rewrite_goals_tac [{\it def}]);} It unfolds definitions in the
+  subgoals (but not the main goal), by meta-rewriting with the given
+  definition (see also \S\ref{sec:rewrite_goals}).
+  \index{meta-rewriting}
 
 \item[\ttindexbold{bws}] 
 is like {\tt bw} but takes a list of definitions.
@@ -433,10 +435,10 @@
 executes a proof of the {\it formula\/} in the given {\it theory}, using
 the given tactic function.
 
-\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
-acts like {\tt prove_goal} but also stores the resulting theorem in
-Isabelle's theorem database and in the {\ML} variable $name$ (see
-\S\ref{ExtractingAndStoringTheProvedTheorem}).
+\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts
+  like {\tt prove_goal} but also stores the resulting theorem in the
+  theorem database associated with its theory and in the {\ML}
+  variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}).
 
 \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
       {\it tacsf};]\index{meta-rewriting}
@@ -528,7 +530,7 @@
 \end{ttdescription}
 
 
-\section{Debugging and inspecting}
+\section{*Debugging and inspecting}
 \index{tactics!debugging}
 These functions can be useful when you are debugging a tactic.  They refer
 to the current proof state stored in the subgoal module.  A tactic
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/introduction.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -29,20 +29,19 @@
 
 \medskip Let $\langle isabellehome \rangle$ denote the location where
 the distribution has been installed.  To run Isabelle from a the shell
-prompt within an ordinary text terminal session, simply type:
+prompt within an ordinary text terminal session, simply type
 \begin{ttbox}
 \({\langle}isabellehome{\rangle}\)/bin/isabelle
 \end{ttbox}
 This should start an interactive \ML{} session with the default
-object-logic already preloaded.  All Isabelle commands are bound to
-\ML{} identifiers.
+object-logic already preloaded.
 
 Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
 has been added to your shell's search path, in order to avoid typing
 full path specifications of the executable files.
 
 The object-logic image to load may be also specified explicitly as an
-argument to the {\tt isabelle} command, e.g.:
+argument to the {\tt isabelle} command, e.g.
 \begin{ttbox}
 isabelle FOL
 \end{ttbox}
@@ -50,15 +49,15 @@
 (assuming that {\FOL} has been pre-built).
 
 \index{saving your work|bold} Isabelle provides no means of storing
-theorems or proofs on files.  Theorems are simply part of the \ML{}
-state and are named by \ML{} identifiers.  To save your work between
-sessions, you must dump the \ML{} system state to a file.  This is done
-automatically when ending the session normally (e.g.\ by typing
-control-D), provided that the image has been opened \emph{writable} in
-the first place.  The standard object-logics are usually read-only, so
-you probably have to create a private working copy first.  For example,
-the following shell command puts you into a writable Isabelle session
-of name \texttt{Foo} that initially contains just \FOL:
+theorems or internal proof objects on files.  Theorems are simply part
+of the \ML{} state.  To save your work between sessions, you must dump
+the \ML{} system state to a file.  This is done automatically when
+ending the session normally (e.g.\ by typing control-D), provided that
+the image has been opened \emph{writable} in the first place.  The
+standard object-logic images are usually read-only, so you probably
+have to create a private working copy first.  For example, the
+following shell command puts you into a writable Isabelle session of
+name \texttt{Foo} that initially contains just \FOL:
 \begin{ttbox}
 isabelle FOL Foo
 \end{ttbox}
@@ -72,8 +71,8 @@
 isabelle Foo  
 \end{ttbox}
 
-More details about \texttt{isabelle} may be found in the \emph{System
-  Manual}.
+More details about the \texttt{isabelle} command may be found in the
+\emph{System Manual}.
 
 \medskip Saving the state is not enough.  Record, on a file, the
 top-level commands that generate your theories and proofs.  Such a
@@ -87,10 +86,8 @@
 \texttt{Isabelle} executable (note the capital I) runs one such
 interface, depending on your local configuration.  Furthermore there
 are a number of external utilities available.  These are started
-uniformly via the \texttt{isatool} wrapper.
-
-Again, see the \emph{System Manual} for more information user
-interfaces and utilities.
+uniformly via the \texttt{isatool} wrapper.  See the \emph{System
+  Manual} for more information user interfaces and utilities.
 
 
 \section{Ending a session}
@@ -102,9 +99,9 @@
 \begin{ttdescription}
 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
   the state.
-
-\item[\ttindexbold{exit}();] same as {\tt quit}, passing a return code
-  to the operating system.
+  
+\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
+  code \(i\) to the operating system.
 
 \item[\ttindexbold{commit}();] saves the current state without ending
   the session, provided that the logic image is opened read-write.
@@ -123,11 +120,11 @@
 time_use        : string -> unit
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{cd} "{\it dir}";]
-  changes the current directory to {\it dir}.  This is the default directory
-  for reading files and for writing temporary files.
-
-\item[\ttindexbold{pwd}();] returns the path of the current directory.
+\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
+  {\it dir}.  This is the default directory for reading files.
+  
+\item[\ttindexbold{pwd}();] returns the full path of the current
+  directory.
 
 \item[\ttindexbold{use} "$file$";]  
 reads the given {\it file} as input to the \ML{} session.  Reading a file
@@ -139,8 +136,8 @@
 
 The $dir$ and $file$ specifications of the \texttt{cd} and
 \texttt{use} commands may contain path variables that are expanded
-accordingly --- e.g.\ \texttt{\$ISABELLE_HOME}, or \texttt{\~\relax}
-(abbreviating \texttt{\$HOME}).  Section~\ref{LoadingTheories}
+appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
+(which abbreviates \texttt{\$HOME}).  Section~\ref{LoadingTheories}
 describes commands for loading theory files.
 
 
@@ -164,8 +161,9 @@
 Pretty.setmargin : int -> unit
 print_depth      : int -> unit
 \end{ttbox}
-These set limits for terminal output.  See also {\tt goals_limit}, which
-limits the number of subgoals printed (page~\pageref{sec:goals-printing}).
+These set limits for terminal output.  See also {\tt goals_limit},
+which limits the number of subgoals printed
+(\S\ref{sec:goals-printing}).
 
 \begin{ttdescription}
 \item[\ttindexbold{Pretty.setdepth} \(d\);]  
@@ -176,7 +174,7 @@
 
 \item[\ttindexbold{Pretty.setmargin} \(m\);]  
   tells Isabelle's pretty printer to assume a right margin (page width)
-  of~$m$.  The initial margin is~80.
+  of~$m$.  The initial margin is~76.
 
 \item[\ttindexbold{print_depth} \(n\);]  
   limits the printing depth of complex \ML{} values, such as theorems and
@@ -185,7 +183,7 @@
 \end{ttdescription}
 
 
-\subsection{Printing of hypotheses, brackets, types and sorts}
+\subsection{Printing of hypotheses, brackets, types etc.}
 \index{meta-assumptions!printing of}
 \index{types!printing of}\index{sorts!printing of}
 \begin{ttbox} 
@@ -193,27 +191,38 @@
 show_brackets : bool ref \hfill{\bf initially false}
 show_types    : bool ref \hfill{\bf initially false}
 show_sorts    : bool ref \hfill{\bf initially false}
+show_consts   : bool ref \hfill{\bf initially false}
 \end{ttbox}
 These flags allow you to control how much information is displayed for
-terms and theorems.  The hypotheses are normally shown; superfluous
-parentheses are not.  Types and sorts are normally hidden.  Displaying
-types and sorts may explain why a polymorphic inference rule fails to
-resolve with some goal.
+types, terms and theorems.  The hypotheses of theorems \emph{are}
+normally shown.  Superfluous parentheses of types and terms are not.
+Types and sorts of variables are normally hidden.
+
+Note that displaying types and sorts may explain why a polymorphic
+inference rule fails to resolve with some goal, or why a rewrite rule
+does not apply as expected.
 
 \begin{ttdescription}
-\item[\ttindexbold{show_hyps} := false;]   
-makes Isabelle show each meta-level hypothesis as a dot.
-
-\item[\ttindexbold{show_brackets} := true;] 
-  makes Isabelle show full bracketing.  This reveals the
-  grouping of infix operators.
+\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
+  meta-level hypothesis as a dot.
+  
+\item[set \ttindexbold{show_brackets};] makes Isabelle show full
+  bracketing.  In particular, this reveals the grouping of infix
+  operators.
+  
+\item[set \ttindexbold{show_types};] makes Isabelle show types when
+  printing a term or theorem.
+  
+\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
+  and the sorts of type variables, independently of the value of
+  \texttt{show_types}.
+  
+\item[set \ttindexbold{show_consts};] makes Isabelle show types of
+  constants, provided that showing of types is enabled at all.  This
+  is supported for printing of proof states only.  Note that the
+  output can be enormous as polymorphic constants often occur at
+  several different type instances.
 
-\item[\ttindexbold{show_types} := true;]
-makes Isabelle show types when printing a term or theorem.
-
-\item[\ttindexbold{show_sorts} := true;]
-makes Isabelle show both types and the sorts of type variables.  It does not
-matter whether {\tt show_types} is also~{\tt true}. 
 \end{ttdescription}
 
 
@@ -230,7 +239,7 @@
 form.
 
 \begin{ttdescription}
-\item[\ttindexbold{eta_contract} := true;]
+\item[set \ttindexbold{eta_contract};]
 makes Isabelle perform $\eta$-contractions before printing, so that
 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
 distinction between a term and its $\eta$-expanded form occasionally
@@ -238,6 +247,37 @@
 \end{ttdescription}
 \index{printing control|)}
 
+\section{Diagnostic messages}
+\index{error messages}
+\index{warnings}
+
+Isabelle conceptually provides three output channels for different
+kinds of messages: ordinary text, warnings, errors.  Depending on the
+user interface involved, these messages may appear in different text
+styles or colours, even within separate windows.
+
+The default setup of an \texttt{isabelle} terminal session is as
+follows: plain output of ordinary text, warnings prefixed by
+\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
+typical warning would look like this:
+\begin{ttbox}
+\#\#\# Beware the Jabberwock, my son!
+\#\#\# The jaws that bite, the claws that catch!
+\#\#\# Beware the Jubjub Bird, and shun
+\#\#\# The frumious Bandersnatch!
+\end{ttbox}
+
+\texttt{ML} programs may output diagnostic messages using the
+following functions:
+\begin{ttbox}
+writeln : string -> unit
+warning : string -> unit
+error   : string -> 'a
+\end{ttbox}
+Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
+after having output the text, while \ttindex{writeln} and
+\ttindex{warning} resume normal program execution.
+
 
 \section{Displaying exceptions as error messages}
 \index{exceptions!printing of}
@@ -247,7 +287,7 @@
 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
 and {\tt RSN}, are called both interactively and from programs.  They
 indicate errors not by printing messages, but by raising exceptions.  For
-interactive use, \ML's reporting of an uncaught exception is 
+interactive use, \ML's reporting of an uncaught exception may be
 uninformative.  The Poly/ML function {\tt exception_trace} can generate a
 backtrace.\index{Poly/{\ML} compiler}
 
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/simplifier.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -86,7 +86,7 @@
 
 Using the simplifier effectively may take a bit of experimentation.
 \index{tracing!of simplification}\index{*trace_simp} The tactics can
-be traced by setting \verb$trace_simp := true$.
+be traced by setting \verb$trace_simp$.
 
 There is not just one global current simpset, but one associated with each
 theory as well.  How are these simpset built up?
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/tactic.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -6,9 +6,10 @@
 need to be coded from scratch, as functions; instead they are
 expressed using basic tactics and tacticals.
 
-This chapter only presents the primitive tactics.  Substantial proofs require
-the power of simplification (Chapter~\ref{chap:simplification}) and classical
-reasoning (Chapter~\ref{chap:classical}).
+This chapter only presents the primitive tactics.  Substantial proofs
+require the power of automatic tools like simplification
+(Chapter~\ref{chap:simplification}) and classical tableau reasoning
+(Chapter~\ref{chap:classical}).
 
 \section{Resolution and assumption tactics}
 {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
@@ -251,14 +252,14 @@
 \end{ttdescription}
 
 
-\subsection{Definitions and meta-level rewriting}
+\subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
 \index{definitions}
 
 Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
 constant or a constant applied to a list of variables, for example $\it
-sqr(n)\equiv n\times n$.  (Conditional definitions, $\phi\Imp t\equiv u$,
-are not supported.)  {\bf Unfolding} the definition ${t\equiv u}$ means using
+sqr(n)\equiv n\times n$.  Conditional definitions, $\phi\Imp t\equiv u$,
+are also supported.  {\bf Unfolding} the definition ${t\equiv u}$ means using
 it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
 Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
 no rewrites are applicable to any subterm.
@@ -291,6 +292,12 @@
 folds the {\it defs} throughout the proof state.
 \end{ttdescription}
 
+\begin{warn}
+  These tactics only cope with definitions expressed as meta-level
+  equalities ($\equiv$).  More general equivalences are handled by the
+  simplifier, provided that it is set up appropriately for your logic
+  (see Chapter~\ref{chap:simplification}).
+\end{warn}
 
 \subsection{Theorems useful with tactics}
 \index{theorems!of pure theory}
@@ -356,7 +363,7 @@
 sets the prefix for uniform renaming to~{\it prefix}.  The default prefix
 is {\tt"k"}.
 
-\item[\ttindexbold{Logic.auto_rename} := true;] 
+\item[set \ttindexbold{Logic.auto_rename};] 
 makes Isabelle generate uniform names for parameters. 
 \end{ttdescription}
 
@@ -559,7 +566,7 @@
 \end{ttdescription}
 
 
-\section{*Programming tools for proof strategies}
+\section{Programming tools for proof strategies}
 Do not consider using the primitives discussed in this section unless you
 really need to code tactics from scratch.
 
@@ -626,7 +633,7 @@
 datatype 'a option = None  |  Some of 'a;
 \end{ttbox}
 The {\tt Seq} structure is supposed to be accessed via fully qualified
-names and should not be \texttt{open}ed.
+names and should not be \texttt{open}.
 
 \subsection{Basic operations on sequences}
 \begin{ttbox} 
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/tctical.tex
--- a/doc-src/Ref/tctical.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/tctical.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -96,7 +96,7 @@
 is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
 least once, failing if this is impossible.
 
-\item[\ttindexbold{trace_REPEAT} := true;] 
+\item[set \ttindexbold{trace_REPEAT};] 
 enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
 and {\tt REPEAT}.  To view the tracing options, type {\tt h} at the prompt.
 \end{ttdescription}
@@ -202,7 +202,7 @@
 uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the
 given state.  Thus, it insists upon solving at least one subgoal.
 
-\item[\ttindexbold{trace_DEPTH_FIRST} := true;] 
+\item[set \ttindexbold{trace_DEPTH_FIRST};] 
 enables interactive tracing for {\tt DEPTH_FIRST}.  To view the
 tracing options, type {\tt h} at the prompt.
 \end{ttdescription}
@@ -242,7 +242,7 @@
 contains the result of applying $tac@0$ to the proof state.  This tactical
 permits separate tactics for starting the search and continuing the search.
 
-\item[\ttindexbold{trace_BEST_FIRST} := true;] 
+\item[set \ttindexbold{trace_BEST_FIRST};] 
 enables an interactive tracing mode for the tactical {\tt BEST_FIRST}.  To
 view the tracing options, type {\tt h} at the prompt.
 \end{ttdescription}
@@ -289,11 +289,11 @@
 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may 
 be given to the searching tacticals.
 
-\item[\ttindexbold{eq_thm}($thm1$,$thm2$)] 
-reports whether $thm1$ and $thm2$ are equal.  Both theorems must have
-identical signatures.  Both theorems must have the same conclusions, and
-the same hypotheses, in the same order.  Names of bound variables are
-ignored.
+\item[\ttindexbold{eq_thm} ($thm_1$, $thm_2$)] reports whether $thm_1$
+  and $thm_2$ are equal.  Both theorems must have identical
+  signatures.  Both theorems must have the same conclusions, and the
+  same hypotheses, in the same order.  Names of bound variables are
+  ignored.
 
 \item[\ttindexbold{size_of_thm} $thm$] 
 computes the size of $thm$, namely the number of variables, constants and
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/theories.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -231,7 +231,7 @@
   define a theory.  This list is only used if the theory name in {\tt
     use_thy} does not specify the path explicitly.
 
-\item[\ttindexbold{delete_tmpfiles} := false;]
+\item[reset \ttindexbold{delete_tmpfiles};]
 suppresses the deletion of temporary files.
 \end{ttdescription}
 %
@@ -245,15 +245,15 @@
 to any depth.  One {\tt use_thy} call can read an entire logic
 provided all theories are linked appropriately.
 
-The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
-for the new theory and components for each of the rules.  The structure also
-contains the definitions of the {\tt ML} section, if present.  The file
-{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
-true} and no errors occurred.
+The result is an \ML\ structure~$T$ containing at least a component
+{\tt thy} for the new theory and components for each of the rules.
+The structure also contains the definitions of the {\tt ML} section,
+if present.  The file {\tt.{\it T}.thy.ML} is then deleted if {\tt
+  delete_tmpfiles} is set and no errors occurred.
 
-Finally the file {\it T}{\tt.ML} is read, if it exists.  Since the
-structure $T$ is automatically open in this context, proof scripts may
-(or even should) refer to its components by unqualified names.
+Finally the file {\it T}{\tt.ML} is read, if it exists.  The structure
+$T$ is automatically open in this context.  Proof scripts typically
+refer to its components by unqualified names.
 
 Some applications construct theories directly by calling \ML\ functions.  In
 this situation there is no {\tt.thy} file, only an {\tt.ML} file.  The
@@ -357,31 +357,49 @@
 
 
 \section{Basic operations on theories}\label{BasicOperationsOnTheories}
-\subsection{Extracting an axiom or theorem from a theory}
+\subsection{Retrieving axioms and theorems}
 \index{theories!axioms of}\index{axioms!extracting}
 \index{theories!theorems of}\index{theorems!extracting}
 \begin{ttbox}
-get_axiom : theory -> string -> thm
-get_thm   : theory -> string -> thm
+get_axiom : theory -> xstring -> thm
+get_thm   : theory -> xstring -> thm
+get_thms  : theory -> xstring -> thm list
+axioms_of : theory -> (string * thm) list
+thms_of   : theory -> (string * thm) list
 assume_ax : theory -> string -> thm
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{get_axiom} $thy$ $name$]
-  returns an axiom with the given $name$ from $thy$, raising exception
-  \xdx{THEORY} if none exists.  Merging theories can cause several axioms
-  to have the same name; {\tt get_axiom} returns an arbitrary one.
-
-\item[\ttindexbold{get_thm} $thy$ $name$]
-  is analogous to {\tt get_axiom}, but looks for a stored theorem.  Like
-  {\tt get_axiom} it searches all parents of a theory if the theorem
-  is not associated with $thy$.
-
-\item[\ttindexbold{assume_ax} $thy$ $formula$]
-  reads the {\it formula} using the syntax of $thy$, following the same
-  conventions as axioms in a theory definition.  You can thus pretend that
-  {\it formula} is an axiom and use the resulting theorem like an axiom.
-  Actually {\tt assume_ax} returns an assumption;  \ttindex{result}
-  complains about additional assumptions, but \ttindex{uresult} does not.
+\item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
+  given $name$ from $thy$ or any of its ancestors, raising exception
+  \xdx{THEORY} if none exists.  Merging theories can cause several
+  axioms to have the same name; {\tt get_axiom} returns an arbitrary
+  one.  Usually, axioms are also stored as theorems and may be
+  retrieved via \texttt{get_thm} as well.
+  
+\item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
+    get_axiom}, but looks for a theorem stored in the theory's
+  database.  Like {\tt get_axiom} it searches all parents of a theory
+  if the theorem is not found directly in $thy$.
+  
+\item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
+  for retrieving theorem lists stored within the theory.  It returns a
+  singleton list if $name$ actually refers to a theorem rather than a
+  theorem list.
+  
+\item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
+  node, not including the ones of its ancestors.
+  
+\item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
+  the database of this theory node, not including the ones of its
+  ancestors.
+  
+\item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
+  using the syntax of $thy$, following the same conventions as axioms
+  in a theory definition.  You can thus pretend that {\it formula} is
+  an axiom and use the resulting theorem like an axiom.  Actually {\tt
+    assume_ax} returns an assumption; \ttindex{qed} and
+  \ttindex{result} complain about additional assumptions, but
+  \ttindex{uresult} does not.
 
 For example, if {\it formula} is
 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form
@@ -392,29 +410,34 @@
 \label{BuildingATheory}
 \index{theories!constructing|bold}
 \begin{ttbox}
+ProtoPure.thy  : theory
 Pure.thy       : theory
 CPure.thy      : theory
-merge_theories : theory * theory -> theory
+merge_theories : string -> theory * theory -> theory
 \end{ttbox}
 \begin{description}
-\item[\ttindexbold{Pure.thy}, \ttindexbold{CPure.thy}] contain the
-  syntax and signature of the meta-logic.  There are no axioms:
-  meta-level inferences are carried out by \ML\ functions.  The two
-  \Pure s just differ in their concrete syntax of function
-  application: $t(u@1, \ldots, u@n)$ vs.\ $t\,u@1,\ldots\,u@n$.
-
-\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
-  theories $thy@1$ and $thy@2$.  The resulting theory contains all of the
-  syntax, signature and axioms of the constituent theories.  Merging theories
-  that contain different identification stamps of the same name fails with
+\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
+  \ttindexbold{CPure.thy}] contain the syntax and signature of the
+  meta-logic.  There are basically no axioms: meta-level inferences
+  are carried out by \ML\ functions.  \texttt{Pure} and \texttt{CPure}
+  just differ in their concrete syntax of prefix function application:
+  $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
+  \texttt{CPure}.  \texttt{ProtoPure} is their common parent,
+  containing no syntax for printing prefix applications at all!
+  
+\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
+  the two theories $thy@1$ and $thy@2$, creating a new named theory
+  node.  The resulting theory contains all of the syntax, signature
+  and axioms of the constituent theories.  Merging theories that
+  contain different identification stamps of the same name fails with
   the following message
 \begin{ttbox}
 Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
 \end{ttbox}
-  This error may especially occur when a theory is redeclared --- say to
-  change an incorrect axiom --- and bindings to old versions persist.
-  Isabelle ensures that old and new theories of the same name are not
-  involved in a proof.
+This error may especially occur when a theory is redeclared --- say to
+change an inappropriate definition --- and bindings to old versions
+persist.  Isabelle ensures that old and new theories of the same name
+are not involved in a proof.
 
 %% FIXME
 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
@@ -464,13 +487,13 @@
 \subsection{Inspecting a theory}\label{sec:inspct-thy}
 \index{theories!inspecting|bold}
 \begin{ttbox}
-print_syntax  : theory -> unit
-print_theory  : theory -> unit
-axioms_of     : theory -> (string * thm) list
-thms_of       : theory -> (string * thm) list
-parents_of    : theory -> theory list
-sign_of       : theory -> Sign.sg
-stamps_of_thy : theory -> string ref list
+print_syntax        : theory -> unit
+print_theory        : theory -> unit
+print_data          : theory -> string -> unit
+parents_of          : theory -> theory list
+ancestors_of        : theory -> theory list
+sign_of             : theory -> Sign.sg
+Sign.stamp_names_of : Sign.sg -> string list
 \end{ttbox}
 These provide means of viewing a theory's components.
 \begin{ttdescription}
@@ -480,23 +503,27 @@
   
 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of
   $thy$, excluding the syntax.
-
-\item[\ttindexbold{axioms_of} $thy$]
-returns the additional axioms of the most recent extend node of~$thy$.
-
-\item[\ttindexbold{thms_of} $thy$]
-returns all theorems that are associated with $thy$.
+  
+\item[\ttindexbold{print_data} $thy$ $kind$] prints generic data of
+  $thy$.  This invokes the print method associated with $kind$.  Refer
+  to the output of \texttt{print_theory} for a list of available data
+  kinds in $thy$.
+  
+\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
+  of~$thy$.
+  
+\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
+  (not including $thy$ itself).
+  
+\item[\ttindexbold{sign_of} $thy$] returns the signature associated
+  with~$thy$.  It is useful with functions like {\tt
+    read_instantiate_sg}, which take a signature as an argument.
+  
+\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
+  returns the names of the identification \rmindex{stamps} of ax
+  signature.  These coincide with the names of its full ancestry
+  including that of $sg$ itself.
 
-\item[\ttindexbold{parents_of} $thy$]
-returns the direct ancestors of~$thy$.
-
-\item[\ttindexbold{sign_of} $thy$]
-returns the signature associated with~$thy$.  It is useful with functions
-like {\tt read_instantiate_sg}, which take a signature as an argument.
-
-\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
-returns the identification \rmindex{stamps} of the signature associated
-with~$thy$.
 \end{ttdescription}
 
 
@@ -515,16 +542,16 @@
               | op $  of term * term;
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold}
+\item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
   is the {\bf constant} with name~$a$ and type~$T$.  Constants include
   connectives like $\land$ and $\forall$ as well as constants like~0
   and~$Suc$.  Other constants may be required to define a logic's concrete
   syntax.
 
-\item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold}
+\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
   is the {\bf free variable} with name~$a$ and type~$T$.
 
-\item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold}
+\item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
   is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
   \mltydx{indexname} is a string paired with a non-negative index, or
   subscript; a term's scheme variables can be systematically renamed by
@@ -538,7 +565,7 @@
   more information see de Bruijn \cite{debruijn72} or
   Paulson~\cite[page~336]{paulson91}.
 
-\item[\ttindexbold{Abs}($a$, $T$, $u$)]
+\item[\ttindexbold{Abs} ($a$, $T$, $u$)]
   \index{lambda abs@$\lambda$-abstractions|bold}
   is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
   variable has name~$a$ and type~$T$.  The name is used only for parsing
@@ -555,7 +582,7 @@
 \end{ttbox}
 
 
-\section{Variable binding}
+\section{*Variable binding}
 \begin{ttbox}
 loose_bnos     : term -> int list
 incr_boundvars : int -> term -> term
@@ -691,7 +718,7 @@
 fun S --> T = Type ("fun", [S, T]);
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold}
+\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
   applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
   Type constructors include~\tydx{fun}, the binary function space
   constructor, as well as nullary type constructors such as~\tydx{prop}.
@@ -699,10 +726,10 @@
   patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
   types.
 
-\item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold}
+\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
   is the {\bf type variable} with name~$a$ and sort~$s$.
 
-\item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold}
+\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
   is the {\bf type unknown} with indexname~$v$ and sort~$s$.
   Type unknowns are essentially free type variables, but may be
   instantiated during unification.
@@ -743,7 +770,7 @@
 \end{ttdescription}
 
 
-\section{Oracles: calling external reasoners }
+\section{Oracles: calling trusted external reasoners}
 \label{sec:oracles}
 \index{oracles|(}
 
@@ -756,19 +783,21 @@
 depends upon oracle calls.
 
 \begin{ttbox}
-     invoke_oracle : theory * Sign.sg * exn -> thm
-     set_oracle    : (Sign.sg * exn -> term) -> theory -> theory
+invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
+Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory -> theory
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle
-  of theory $thy$ passing the information contained in the exception value
-  $exn$ and creating a theorem having signature $sign$.  Errors arise if $thy$
-  does not have an oracle, if the oracle rejects its arguments or if its
-  result is ill-typed.
-
-\item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to
-  be $fn$.  It is seldom called explicitly, as there is syntax for oracles in
-  theory files.  Any theory node can have at most one oracle.
+\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
+  invokes the oracle $name$ of theory $thy$ passing the information
+  contained in the exception value $data$ and creating a theorem
+  having signature $sign$.  Note that type \ttindex{object} is just an
+  abbreviation for \texttt{exn}.  Errors arise if $thy$ does not have
+  an oracle called $name$, if the oracle rejects its arguments or if
+  its result is ill-typed.
+  
+\item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends
+  $thy$ by oracle $fun$ called $name$.  It is seldom called
+  explicitly, as there is concrete syntax for oracles in theory files.
 \end{ttdescription}
 
 A curious feature of {\ML} exceptions is that they are ordinary constructors.
@@ -780,7 +809,7 @@
 There must be some way of invoking the external reasoner from \ML, either
 because it is coded in {\ML} or via an operating system interface.  Isabelle
 expects the {\ML} function to take two arguments: a signature and an
-exception.
+exception object.
 \begin{itemize}
 \item The signature will typically be that of a desendant of the theory
   declaring the oracle.  The oracle will use it to distinguish constants from
@@ -793,49 +822,54 @@
   solve the specified problem.
 \end{itemize}
 
-A trivial example is provided on directory {\tt FOL/ex}.  This oracle
-generates tautologies of the form $P\bimp\cdots\bimp P$, with an even number
-of $P$s. 
+A trivial example is provided in theory {\tt FOL/ex/IffOracle}.  This
+oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
+an even number of $P$s.
 
-File {\tt declIffOracle.ML} begins by declaring a new exception constructor
-for the oracle the information it requires: here, just an integer.  It
-contains some code (suppressed below) for creating the tautologies, and
-finally declares the oracle function itself:
+The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring
+a few auxiliary functions (suppressed below) for creating the
+tautologies.  Then it declares a new exception constructor for the
+information required by the oracle: here, just an integer. It finally
+defines the oracle function itself.
 \begin{ttbox}
-exception IffOracleExn of int;
-\(\vdots\)
-fun mk_iff_oracle (sign, IffOracleExn n) = 
-    if n>0 andalso n mod 2 = 0 
-    then Trueprop $ mk_iff n
-    else raise IffOracleExn n;
+exception IffOracleExn of int;\medskip
+fun mk_iff_oracle (sign, IffOracleExn n) =
+  if n > 0 andalso n mod 2 = 0
+  then Trueprop $ mk_iff n
+  else raise IffOracleExn n;
 \end{ttbox}
-Observe the function two arguments, the signature {\tt sign} and the exception
-given as a pattern.  The function checks its argument for validity.  If $n$ is
-positive and even then it creates a tautology containing $n$ occurrences
-of~$P$.  Otherwise it signals error by raising its own exception.  Errors may
-be signalled by other means, such as returning the theorem {\tt True}.
-Please ensure that the oracle's result is correctly typed; Isabelle will
-reject ill-typed theorems by raising a cryptic exception at top level.
+Observe the function's two arguments, the signature {\tt sign} and the
+exception given as a pattern.  The function checks its argument for
+validity.  If $n$ is positive and even then it creates a tautology
+containing $n$ occurrences of~$P$.  Otherwise it signals error by
+raising its own exception (just by happy coincidence).  Errors may be
+signalled by other means, such as returning the theorem {\tt True}.
+Please ensure that the oracle's result is correctly typed; Isabelle
+will reject ill-typed theorems by raising a cryptic exception at top
+level.
 
-The theory file {\tt IffOracle.thy} packages up the function above as an
-oracle.  The first line indicates that the new theory depends upon the file
-{\tt declIffOracle.ML} (which declares the {\ML} code) as well as on \FOL.
-The second line informs Isabelle that this theory has an oracle given by the
-function {\tt mk_iff_oracle}.
+The \texttt{oracle} section of {\tt IffOracle.thy} installs above
+\texttt{ML} function as follows:
 \begin{ttbox}
-IffOracle = "declIffOracle" + FOL +
-oracle mk_iff_oracle
+IffOracle = FOL +\medskip
+oracle
+  iff = mk_iff_oracle\medskip
 end
 \end{ttbox}
-Because a theory can have at most one oracle, the theory itself serves to
-identify the oracle.
 
-Here are some examples of invoking the oracle.  An argument of 10 is allowed,
-but one of 5 is forbidden:
+Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
+the oracle:
 \begin{ttbox}
-invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
+fun iff_oracle n =
+  invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
+\end{ttbox}
+
+Here are some example applications of the \texttt{iff} oracle.  An
+argument of 10 is allowed, but one of 5 is forbidden:
+\begin{ttbox}
+iff_oracle 10;
 {\out  "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
-invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5); 
+iff_oracle 5;
 {\out Exception- IffOracleExn 5 raised}
 \end{ttbox}
 
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/theory-syntax.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -130,7 +130,7 @@
 witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim)
         ;
 
-oracle : 'oracle' name
+oracle : 'oracle' name '=' name
        ;
 
 ml : 'ML' text
diff -r 86ac9153e660 -r 7264fa2ff2ec doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/thm.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -135,9 +135,10 @@
 \subsection{Instantiating a theorem}
 \index{instantiation}
 \begin{ttbox}
-read_instantiate    :            (string * string) list -> thm -> thm
-read_instantiate_sg : Sign.sg -> (string * string) list -> thm -> thm
-cterm_instantiate   :              (cterm * cterm) list -> thm -> thm
+read_instantiate    :                (string * string) list -> thm -> thm
+read_instantiate_sg :     Sign.sg -> (string * string) list -> thm -> thm
+cterm_instantiate   :                  (cterm * cterm) list -> thm -> thm
+instantiate'        : ctyp option list -> cterm option list -> thm -> thm
 \end{ttbox}
 These meta-rules instantiate type and term unknowns in a theorem.  They are
 occasionally useful.  They can prevent difficulties with higher-order
@@ -166,6 +167,15 @@
 \item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}] 
 is similar to {\tt read_instantiate}, but the instantiations are provided
 as pairs of certified terms, not as strings to be read.
+
+\item[\ttindexbold{instantiate'} {\it ctyps} {\it cterms} {\it thm}]
+  instantiates {\it thm} according to the positional arguments {\it
+    ctyps} and {\it cterms}.  Counting from left to right, schematic
+  variables $?x$ are either replaced by $t$ for any argument
+  \texttt{Some\(\;t\)}, or left unchanged in case of \texttt{None} or
+  if the end of the argument list is encountered.  Types are
+  instantiated before terms.
+
 \end{ttdescription}
 
 
@@ -208,46 +218,62 @@
 \index{theorems!taking apart}
 \index{flex-flex constraints}
 \begin{ttbox} 
+cprop_of      : thm -> cterm
 concl_of      : thm -> term
 prems_of      : thm -> term list
+cprems_of     : thm -> cterm list
 nprems_of     : thm -> int
-tpairs_of     : thm -> (term*term)list
-stamps_of_thy : thm -> string ref list
+tpairs_of     : thm -> (term * term) list
+sign_of_thm   : thm -> Sign.sg
 theory_of_thm : thm -> theory
-dest_state    : thm*int -> (term*term)list*term list*term*term
-rep_thm       : thm -> {\ttlbrace}prop: term, hyps: term list, der: deriv, 
-                        maxidx: int, sign: Sign.sg, shyps: sort list\ttrbrace
+dest_state    : thm * int -> (term * term) list * term list * term * term
+rep_thm       : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
+                        shyps: sort list, hyps: term list, prop: term\ttrbrace
+crep_thm      : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
+                        shyps: sort list, hyps: cterm list, prop: cterm\ttrbrace
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{concl_of} $thm$] 
-returns the conclusion of $thm$ as a term.
-
-\item[\ttindexbold{prems_of} $thm$] 
-returns the premises of $thm$ as a list of terms.
+\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
+  a certified term.
+  
+\item[\ttindexbold{concl_of} $thm$] returns the conclusion of $thm$ as
+  a term.
+  
+\item[\ttindexbold{prems_of} $thm$] returns the premises of $thm$ as a
+  list of terms.
+  
+\item[\ttindexbold{cprems_of} $thm$] returns the premises of $thm$ as
+  a list of certified terms.
 
 \item[\ttindexbold{nprems_of} $thm$] 
 returns the number of premises in $thm$, and is equivalent to {\tt
-  length(prems_of~$thm$)}.
-
-\item[\ttindexbold{tpairs_of} $thm$] 
-returns the flex-flex constraints of $thm$.
+  length~(prems_of~$thm$)}.
 
-\item[\ttindexbold{stamps_of_thm} $thm$] 
-returns the \rmindex{stamps} of the signature associated with~$thm$.
-
-\item[\ttindexbold{theory_of_thm} $thm$]
-returns the theory associated with $thm$.
+\item[\ttindexbold{tpairs_of} $thm$] returns the flex-flex constraints
+  of $thm$.
+  
+\item[\ttindexbold{sign_of_thm} $thm$] returns the signature
+  associated with $thm$.
+  
+\item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated
+  with $thm$.  Note that this does a lookup in Isabelle's global
+  database of loaded theories.
 
 \item[\ttindexbold{dest_state} $(thm,i)$] 
 decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
 list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
 (this will be an implication if there are more than $i$ subgoals).
 
-\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record containing the
-  statement of~$thm$ ({\tt prop}), its list of meta-assumptions ({\tt hyps}),
-  its derivation ({\tt der}), a bound on the maximum subscript of its
-  unknowns ({\tt maxidx}), and its signature ({\tt sign}).  The {\tt shyps}
-  field is discussed below.
+\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record
+  containing the statement of~$thm$ ({\tt prop}), its list of
+  meta-assumptions ({\tt hyps}), its derivation ({\tt der}), a bound
+  on the maximum subscript of its unknowns ({\tt maxidx}), and a
+  reference to its signature ({\tt sign_ref}).  The {\tt shyps} field
+  is discussed below.
+  
+\item[\ttindexbold{crep_thm} $thm$] like \texttt{rep_thm}, but returns
+  the hypotheses and statement as certified terms.
+
 \end{ttdescription}
 
 
@@ -267,7 +293,7 @@
 syntactic classification of types --- for example, FOL distinguishes between
 terms and other types.  But when type classes are introduced through axioms,
 this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
-a type belonging to it because certain axioms are unsatisfiable.
+a type belonging to it because certain sets of axioms are unsatisfiable.
 
 If a theorem contains a type variable that is constrained by an empty
 sort, then that theorem has no instances.  It is basically an instance
@@ -301,10 +327,10 @@
 unexpectedly.  Letting {\tt res_inst_tac} circumvent the problem is easier,
 though.
 \begin{ttdescription}
-\item[Unify.trace_simp := true;] 
+\item[set Unify.trace_simp;] 
 causes tracing of the simplification phase.
 
-\item[Unify.trace_types := true;] 
+\item[set Unify.trace_types;] 
 generates warnings of incompleteness, when unification is not considering
 all possible instantiations of type unknowns.
 
@@ -313,22 +339,23 @@
 Use $n=0$ for full tracing.  At the default value of~10, tracing
 information is almost never printed.
 
-\item[Unify.search_bound := $n$;] 
-causes unification to limit its search to depth~$n$.  Because of this
-bound, higher-order unification cannot return an infinite sequence, though
-it can return a very long one.  The search rarely approaches the default
-value of~20.  If the search is cut off, unification prints {\tt
-***Unification bound exceeded}.
+\item[Unify.search_bound := $n$;] causes unification to limit its
+  search to depth~$n$.  Because of this bound, higher-order
+  unification cannot return an infinite sequence, though it can return
+  a very long one.  The search rarely approaches the default value
+  of~20.  If the search is cut off, unification prints a warning
+  \texttt{Unification bound exceeded}.
 \end{ttdescription}
 
 
-\section{Primitive meta-level inference rules}
+\section{*Primitive meta-level inference rules}
 \index{meta-rules|(}
-These implement the meta-logic in {\sc lcf} style, as functions from theorems
-to theorems.  They are, rarely, useful for deriving results in the pure
-theory.  Mainly, they are included for completeness, and most users should
-not bother with them.  The meta-rules raise exception \xdx{THM} to signal
-malformed premises, incompatible signatures and similar errors.
+These implement the meta-logic in the style of the {\sc lcf} system,
+as functions from theorems to theorems.  They are, rarely, useful for
+deriving results in the pure theory.  Mainly, they are included for
+completeness, and most users should not bother with them.  The
+meta-rules raise exception \xdx{THM} to signal malformed premises,
+incompatible signatures and similar errors.
 
 \index{meta-assumptions}
 The meta-logic uses natural deduction.  Each theorem may depend on
@@ -694,7 +721,7 @@
 omitting bookkeeping steps that have no logical meaning to an outside
 observer.  Rewriting steps are recorded in similar detail as the output of
 simplifier tracing.  The proof object can be inspected by a separate
-proof-checker, or used to generate human-readable proof digests.
+proof-checker, for example.
 
 Full proof objects are large.  They multiply storage requirements by about
 seven; attempts to build large logics (such as {\sc zf} and {\sc hol}) may
@@ -727,10 +754,11 @@
 record: 
 \begin{ttbox} 
 #der (rep_thm conjI);
-{\out Join (Theorem "conjI", [Join (MinProof,[])]) : deriv}
+{\out Join (Theorem "HOL.conjI", [Join (MinProof,[])]) : deriv}
 \end{ttbox}
-This proof object identifies a labelled theorem, {\tt conjI}, whose underlying
-proof has not been recorded; all we have is {\tt MinProof}.
+This proof object identifies a labelled theorem, {\tt conjI} of theory
+\texttt{HOL}, whose underlying proof has not been recorded; all we
+have is {\tt MinProof}.
 
 Nontrivial proof objects are unreadably large and complex.  Isabelle provides
 several functions to help you inspect them informally.  These functions omit