theory loader stuff updated and improved;

--- a/doc-src/Ref/introduction.tex	Mon May 03 14:43:52 1999 +0200
+++ b/doc-src/Ref/introduction.tex	Mon May 03 18:35:48 1999 +0200
@@ -15,17 +15,17 @@
 finally esoteric functions.  Use the Index when you are looking for the
 definition of a particular Isabelle function.
 
-A few examples are presented.  Many examples files are distributed with
+A few examples are presented.  Many example files are distributed with
 Isabelle, however; please experiment interactively.
 
 
 \section{Basic interaction with Isabelle}
 \index{starting up|bold}\nobreak
 %
-We assume that your local Isabelle administrator (this might be you!)
-has already installed the \Pure\ system and several object-logics
-properly --- otherwise see the {\tt INSTALL} file in the top-level
-directory of the distribution on how to build it.
+We assume that your local Isabelle administrator (this might be you!) has
+already installed the Isabelle system together with appropriate object-logics
+--- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
+top-level directory of the distribution on how to do this.
 
 \medskip Let $\langle isabellehome \rangle$ denote the location where
 the distribution has been installed.  To run Isabelle from a the shell
@@ -33,61 +33,67 @@
 \begin{ttbox}
 \({\langle}isabellehome{\rangle}\)/bin/isabelle
 \end{ttbox}
-This should start an interactive \ML{} session with the default
-object-logic already preloaded.
+This should start an interactive \ML{} session with the default object-logic
+(usually {\HOL}) already pre-loaded.
 
-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.
+Subsequently, we assume that the \texttt{isabelle} executable is determined
+automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
+  \rangle\)/bin} to your search path.\footnote{Depending on your installation,
+  there might be also stand-alone binaries located in some global directory
+  such as \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle
+    isabellehome \rangle\)/bin/isabelle}, though!  See \texttt{isatool
+    install} in \emph{The Isabelle System Manual} of how to do this properly.}
 
-The object-logic image to load may be also specified explicitly as an
-argument to the {\tt isabelle} command, e.g.
+The object-logic image to load may be also specified explicitly as an argument
+to the {\tt isabelle} command, e.g.
 \begin{ttbox}
 isabelle FOL
 \end{ttbox}
-This should put you into the world of polymorphic first-order logic
-(assuming that {\FOL} has been pre-built).
+This should put you into the world of polymorphic first-order logic (assuming
+that an image of {\FOL} has been pre-built).
 
-\index{saving your work|bold} Isabelle provides no means of storing
-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:
+\index{saving your session|bold} Isabelle provides no means of storing
+theorems or internal proof objects on files.  Theorems are simply part of the
+\ML{} state.  To save your work between sessions, you may 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 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 plain \HOL:
 \begin{ttbox}
-isabelle FOL Foo
+isabelle HOL Foo
 \end{ttbox}
 Ending the \texttt{Foo} session with control-D will cause the complete
-\ML{} world to be saved somewhere in your home directory\footnote{The
-  default location is in \texttt{\~\relax/isabelle/heaps}, but this
-  depends on your local configuration.}.  Make sure there is enough
-space available! Then one may later continue at exactly the same point
-by running
+\ML-world to be saved somewhere in your home directory\footnote{The default
+  location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
+  local configuration.}.  Make sure there is enough space available! Then one
+may later continue at exactly the same point by running
 \begin{ttbox}
 isabelle Foo  
 \end{ttbox}
 
-More details about the \texttt{isabelle} command may be found in \emph{The
-  Isabelle System Manual}.
+\medskip Saving the {\ML} state is not enough.  Record, on a file, the
+top-level commands that generate your theories and proofs.  Such a record
+allows you to replay the proofs whenever required, for instance after making
+minor changes to the axioms.  Ideally, your these sources will be somewhat
+intelligible to others as a formal description of your work.
 
-\medskip Saving the state is not enough.  Record, on a file, the
-top-level commands that generate your theories and proofs.  Such a
-record allows you to replay the proofs whenever required, for instance
-after making minor changes to the axioms.  Ideally, your record will
-be somewhat intelligible to others as a formal description of your
-work.
+It is good practice to put all source files that constitute a separate
+Isabelle session into an individual directory, together with an {\ML} file
+called \texttt{ROOT.ML} that contains appropriate commands to load all other
+files required.  Running \texttt{isabelle} with option \texttt{-u}
+automatically loads \texttt{ROOT.ML} on entering the session.  The
+\texttt{isatool usedir} utility provides some more options to manage your
+sessions, such as automatic generation of theory browsing information.
 
-\medskip There are more comfortable user interfaces than the
-bare-bones \ML{} top-level run from a text terminal.  The
-\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.  See the \emph{System
-  Manual} for more information user interfaces and utilities.
+\medskip More details about the \texttt{isabelle} and \texttt{isatool}
+commands may be found in \emph{The Isabelle System Manual}.
+
+\medskip There are more comfortable user interfaces than the bare-bones \ML{}
+top-level run from a text terminal.  The \texttt{Isabelle} executable (note
+the capital I) runs one such interface, depending on your local configuration.
+Again, see \emph{The Isabelle System Manual} for more information.
 
 
 \section{Ending a session}
@@ -139,8 +145,55 @@
 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
 expanded appropriately.  Note that \texttt{\~\relax} abbreviates
 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
-\texttt{\$ISABELLE_HOME}.  Section~\ref{LoadingTheories} describes commands
-for loading theory files.
+\texttt{\$ISABELLE_HOME}.
+
+
+\section{Reading theories}\label{sec:intro-theories}
+\index{theories!reading}
+
+In Isabelle, any kind of declarations, definitions, etc.\ are organized around
+named \emph{theory} objects.  Logical reasoning always takes place within a
+certain theory context, which may be switched at any time.  Theory $name$ is
+defined by a theory file $name$\texttt{.thy}, containing declarations of
+\texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
+\S\ref{sec:ref-defining-theories} for more details on concrete syntax).
+Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
+proof scripts that are to be run in the context of the theory.
+
+\begin{ttbox}
+context      : theory -> unit
+the_context  : unit -> theory
+theory       : string -> theory
+use_thy      : string -> unit
+time_use_thy : string -> unit
+\end{ttbox}
+
+\begin{ttdescription}
+  
+\item[\ttindexbold{context} $thy$;] switches the current theory context.  Any
+  subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
+  will refer to $thy$ as its theory.
+  
+\item[\ttindexbold{the_context}();] obtains the current theory context, or
+  raises an error if absent.
+  
+\item[\ttindexbold{theory} $name$;] retrieves the theory called $name$ from
+  the internal database of loaded theories, raising an error if absent.
+  
+\item[\ttindexbold{use_thy} $name$;] reads theory $name$ from the file system,
+  looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML}; also
+  makes sure that all parent theories are loaded as well.  In case some older
+  versions have already been present, \texttt{use_thy} only tries to reload
+  $name$ itself, but is content with any version of its parents.
+  
+\item[\ttindexbold{time_use_thy} $name$;] same as \texttt{use_thy}, but
+  reports the time taken to process the actual theory parts and {\ML} files
+  separately.
+  
+\end{ttdescription}
+
+See \S\ref{sec:more-theories} for further information on Isabelle's theory
+loader.
 
 
 \section{Setting flags}
@@ -263,10 +316,9 @@
 \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.
+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.
 
 The default setup of an \texttt{isabelle} terminal session is as
 follows: plain output of ordinary text, warnings prefixed by

--- a/doc-src/Ref/ref.ind	Mon May 03 14:43:52 1999 +0200
+++ b/doc-src/Ref/ref.ind	Mon May 03 18:35:48 1999 +0200
@@ -24,8 +24,9 @@
 
   \item {\tt Abs}, \bold{62}, 88
   \item {\tt abstract_over}, \bold{63}
-  \item {\tt abstract_rule}, \bold{48}
+  \item {\tt abstract_rule}, \bold{49}
   \item {\tt aconv}, \bold{63}
+  \item {\tt add_path}, \bold{59}
   \item {\tt addaltern}, \bold{137}
   \item {\tt addbefore}, \bold{137}
   \item {\tt Addcongs}, \bold{107}
@@ -61,96 +62,96 @@
   \item {\tt addSSolver}, \bold{113}
   \item {\tt addSWrapper}, \bold{137}
   \item {\tt addWrapper}, \bold{137}
-  \item {\tt all_tac}, \bold{33}
-  \item {\tt ALLGOALS}, \bold{37}, 119, 122
+  \item {\tt all_tac}, \bold{34}
+  \item {\tt ALLGOALS}, \bold{38}, 119, 122
   \item ambiguity
     \subitem of parsed expressions, 81
   \item {\tt ancestors_of}, \bold{61}
   \item {\tt any} nonterminal, \bold{70}
-  \item {\tt APPEND}, \bold{31}, 33
-  \item {\tt APPEND'}, 38
+  \item {\tt APPEND}, \bold{32}, 34
+  \item {\tt APPEND'}, 39
   \item {\tt Appl}, 85
   \item {\tt aprop} nonterminal, \bold{72}
-  \item {\tt ares_tac}, \bold{22}
+  \item {\tt ares_tac}, \bold{23}
   \item {\tt args} nonterminal, 95
   \item {\tt Arith} theory, 121
   \item arities
-    \subitem context conditions, 57
+    \subitem context conditions, 58
   \item {\tt Asm_full_simp_tac}, \bold{106}
-  \item {\tt asm_full_simp_tac}, 25, \bold{116}, 120
+  \item {\tt asm_full_simp_tac}, 26, \bold{116}, 120
   \item {\tt asm_full_simplify}, 116
-  \item {\tt asm_rl} theorem, 24
+  \item {\tt asm_rl} theorem, 25
   \item {\tt Asm_simp_tac}, \bold{105}, 118
   \item {\tt asm_simp_tac}, \bold{116}, 128
   \item {\tt asm_simplify}, 116
   \item associative-commutative operators, 121
-  \item {\tt assume}, \bold{47}
-  \item {\tt assume_ax}, 9, \bold{11}
-  \item {\tt assume_tac}, \bold{20}, 134
-  \item {\tt assumption}, \bold{50}
+  \item {\tt assume}, \bold{48}
+  \item {\tt assume_ax}, 10, \bold{12}
+  \item {\tt assume_tac}, \bold{21}, 134
+  \item {\tt assumption}, \bold{51}
   \item assumptions
     \subitem contradictory, 142
-    \subitem deleting, 25
+    \subitem deleting, 26
     \subitem in simplification, 105, 114
-    \subitem inserting, 22
+    \subitem inserting, 23
     \subitem negated, 132
-    \subitem of main goal, 8, 9, 11, 16, 17
+    \subitem of main goal, 9, 10, 12, 17, 18
     \subitem reordering, 120
-    \subitem rotating, 25
+    \subitem rotating, 26
     \subitem substitution in, 102
-    \subitem tactics for, 20
+    \subitem tactics for, 21
   \item ASTs, 85--90
     \subitem made from parse trees, 86
     \subitem made from terms, 88
-  \item {\tt atac}, \bold{22}
+  \item {\tt atac}, \bold{23}
   \item {\tt Auto_tac}, \bold{142}
   \item {\tt auto_tac} $(cs,ss)$, \bold{139}
-  \item {\tt axclass} section, 56
-  \item axiomatic type class, 56
+  \item {\tt axclass} section, 57
+  \item axiomatic type class, 57
   \item axioms
-    \subitem extracting, 10
-  \item {\tt axioms_of}, \bold{10}
+    \subitem extracting, 11
+  \item {\tt axioms_of}, \bold{11}
 
   \indexspace
 
-  \item {\tt ba}, \bold{13}
-  \item {\tt back}, \bold{12}
-  \item batch execution, 15
-  \item {\tt bd}, \bold{13}
-  \item {\tt bds}, \bold{13}
-  \item {\tt be}, \bold{13}
-  \item {\tt bes}, \bold{13}
-  \item {\tt BEST_FIRST}, \bold{34}, 35
+  \item {\tt ba}, \bold{14}
+  \item {\tt back}, \bold{13}
+  \item batch execution, 16
+  \item {\tt bd}, \bold{14}
+  \item {\tt bds}, \bold{14}
+  \item {\tt be}, \bold{14}
+  \item {\tt bes}, \bold{14}
+  \item {\tt BEST_FIRST}, \bold{35}, 36
   \item {\tt Best_tac}, \bold{142}
   \item {\tt best_tac}, \bold{140}
-  \item {\tt beta_conversion}, \bold{48}
-  \item {\tt bicompose}, \bold{51}
-  \item {\tt bimatch_tac}, \bold{26}
-  \item {\tt bind_thm}, \bold{10}, 11, 41
+  \item {\tt beta_conversion}, \bold{49}
+  \item {\tt bicompose}, \bold{52}
+  \item {\tt bimatch_tac}, \bold{27}
+  \item {\tt bind_thm}, \bold{11}, 12, 42
   \item binders, \bold{80}
-  \item {\tt biresolution}, \bold{50}
-  \item {\tt biresolve_tac}, \bold{26}, 143
+  \item {\tt biresolution}, \bold{51}
+  \item {\tt biresolve_tac}, \bold{27}, 143
   \item {\tt Blast.depth_tac}, \bold{139}
   \item {\tt Blast.trace}, \bold{139}
   \item {\tt Blast_tac}, \bold{142}
   \item {\tt blast_tac}, \bold{138}
   \item {\tt Bound}, \bold{62}, 86, 88, 89
   \item {\tt bound_hyp_subst_tac}, \bold{102}
-  \item {\tt br}, \bold{13}
-  \item {\tt BREADTH_FIRST}, \bold{34}
-  \item {\tt brs}, \bold{13}
-  \item {\tt bw}, \bold{14}
-  \item {\tt bws}, \bold{14}
-  \item {\tt by}, \bold{8}, 11--13, 17
-  \item {\tt byev}, \bold{9}
+  \item {\tt br}, \bold{14}
+  \item {\tt BREADTH_FIRST}, \bold{35}
+  \item {\tt brs}, \bold{14}
+  \item {\tt bw}, \bold{15}
+  \item {\tt bws}, \bold{15}
+  \item {\tt by}, \bold{9}, 12--14, 18
+  \item {\tt byev}, \bold{10}
 
   \indexspace
 
   \item {\tt cd}, \bold{3}
   \item {\tt cert_axm}, \bold{64}
-  \item {\tt CHANGED}, \bold{33}
-  \item {\tt chop}, \bold{11}, 16
-  \item {\tt choplev}, \bold{12}
+  \item {\tt CHANGED}, \bold{34}
+  \item {\tt chop}, \bold{12}, 17
+  \item {\tt choplev}, \bold{13}
   \item {\tt Clarify_step_tac}, \bold{142}
   \item {\tt clarify_step_tac}, \bold{139}
   \item {\tt Clarify_tac}, \bold{142}
@@ -162,54 +163,55 @@
   \item {\tt claset} ML type, 135
   \item {\tt ClasimpFun}, 144
   \item classes
-    \subitem context conditions, 57
+    \subitem context conditions, 58
   \item classical reasoner, 130--144
     \subitem setting up, 143
     \subitem tactics, 138
   \item classical sets, 134
   \item {\tt ClassicalFun}, 143
-  \item {\tt combination}, \bold{48}
-  \item {\tt commit}, \bold{2}
-  \item {\tt COMP}, \bold{50}
-  \item {\tt compose}, \bold{50}
-  \item {\tt compose_tac}, \bold{26}
-  \item {\tt concl_of}, \bold{44}
-  \item {\tt COND}, \bold{35}
+  \item {\tt combination}, \bold{49}
+  \item {\tt commit}, \bold{3}
+  \item {\tt COMP}, \bold{51}
+  \item {\tt compose}, \bold{51}
+  \item {\tt compose_tac}, \bold{27}
+  \item {\tt concl_of}, \bold{45}
+  \item {\tt COND}, \bold{36}
   \item congruence rules, 111
   \item {\tt Const}, \bold{62}, 88, 98
   \item {\tt Constant}, 85, 98
   \item constants, \bold{62}
     \subitem for translations, 75
     \subitem syntactic, 90
-  \item {\tt context}, 105
+  \item {\tt context}, \bold{4}, 105
   \item {\tt contr_tac}, \bold{142}
-  \item {\tt could_unify}, \bold{28}
-  \item {\tt cprems_of}, \bold{44}
-  \item {\tt cprop_of}, \bold{43}
-  \item {\tt CPure} theory, 54
-  \item {\tt CPure.thy}, \bold{61}
-  \item {\tt crep_thm}, \bold{44}
+  \item {\tt could_unify}, \bold{29}
+  \item {\tt cprems_of}, \bold{45}
+  \item {\tt cprop_of}, \bold{44}
+  \item {\tt CPure} theory, 55
+  \item {\tt CPure.thy}, \bold{60}
+  \item {\tt crep_thm}, \bold{45}
   \item {\tt cterm} ML type, 64
-  \item {\tt cterm_instantiate}, \bold{42}
-  \item {\tt cterm_of}, 8, 16, \bold{64}
+  \item {\tt cterm_instantiate}, \bold{43}
+  \item {\tt cterm_of}, 9, 17, \bold{64}
   \item {\tt ctyp}, \bold{65}
   \item {\tt ctyp_of}, \bold{66}
-  \item {\tt cut_facts_tac}, \bold{22}, 103
-  \item {\tt cut_inst_tac}, \bold{22}
-  \item {\tt cut_rl} theorem, 24
+  \item {\tt cut_facts_tac}, \bold{23}, 103
+  \item {\tt cut_inst_tac}, \bold{23}
+  \item {\tt cut_rl} theorem, 25
 
   \indexspace
 
   \item {\tt datatype}, 107
   \item {\tt Deepen_tac}, \bold{142}
   \item {\tt deepen_tac}, \bold{140}
-  \item {\tt defer_tac}, \bold{23}
-  \item definitions, \see{rewriting, meta-level}{1}, 23, \bold{57}
-    \subitem unfolding, 8, 9
+  \item {\tt defer_tac}, \bold{24}
+  \item definitions, \see{rewriting, meta-level}{1}, 24, \bold{58}
+    \subitem unfolding, 9, 10
+  \item {\tt del_path}, \bold{59}
   \item {\tt Delcongs}, \bold{107}
   \item {\tt delcongs}, \bold{112}
   \item {\tt deleqcongs}, \bold{112}
-  \item {\tt delete_tmpfiles}, \bold{58}
+  \item {\tt delete_tmpfiles}, \bold{59}
   \item delimiters, \bold{72}, 75, 76, 78
   \item {\tt delloop}, \bold{114}
   \item {\tt delrules}, \bold{135}
@@ -221,58 +223,58 @@
   \item {\tt delSWrapper}, \bold{137}
   \item {\tt delWrapper}, \bold{137}
   \item {\tt dependent_tr'}, 96, \bold{98}
-  \item {\tt DEPTH_FIRST}, \bold{34}
-  \item {\tt DEPTH_SOLVE}, \bold{34}
-  \item {\tt DEPTH_SOLVE_1}, \bold{34}
+  \item {\tt DEPTH_FIRST}, \bold{35}
+  \item {\tt DEPTH_SOLVE}, \bold{35}
+  \item {\tt DEPTH_SOLVE_1}, \bold{35}
   \item {\tt depth_tac}, \bold{140}
-  \item {\tt Deriv.drop}, \bold{52}
-  \item {\tt Deriv.linear}, \bold{52}
-  \item {\tt Deriv.size}, \bold{52}
-  \item {\tt Deriv.tree}, \bold{52}
+  \item {\tt Deriv.drop}, \bold{53}
+  \item {\tt Deriv.linear}, \bold{53}
+  \item {\tt Deriv.size}, \bold{53}
+  \item {\tt Deriv.tree}, \bold{53}
   \item {\tt dest_eq}, \bold{103}
   \item {\tt dest_imp}, \bold{103}
-  \item {\tt dest_state}, \bold{44}
+  \item {\tt dest_state}, \bold{45}
   \item {\tt dest_Trueprop}, \bold{103}
-  \item destruct-resolution, 20
-  \item {\tt DETERM}, \bold{35}
-  \item discrimination nets, \bold{27}
-  \item {\tt distinct_subgoals_tac}, \bold{25}
-  \item {\tt dmatch_tac}, \bold{20}
+  \item destruct-resolution, 21
+  \item {\tt DETERM}, \bold{36}
+  \item discrimination nets, \bold{28}
+  \item {\tt distinct_subgoals_tac}, \bold{26}
+  \item {\tt dmatch_tac}, \bold{21}
   \item {\tt domain_type}, \bold{104}
-  \item {\tt dres_inst_tac}, \bold{21}
-  \item {\tt dresolve_tac}, \bold{20}
-  \item {\tt dtac}, \bold{22}
+  \item {\tt dres_inst_tac}, \bold{22}
+  \item {\tt dresolve_tac}, \bold{21}
+  \item {\tt dtac}, \bold{23}
   \item {\tt dummyT}, 88, 89, 99
   \item duplicate subgoals
-    \subitem removing, 25
+    \subitem removing, 26
 
   \indexspace
 
-  \item elim-resolution, 19
-  \item {\tt ematch_tac}, \bold{20}
+  \item elim-resolution, 20
+  \item {\tt ematch_tac}, \bold{21}
   \item {\tt empty} constant, 94
   \item {\tt empty_cs}, \bold{135}
   \item {\tt empty_ss}, \bold{109}
-  \item {\tt eq_assume_tac}, \bold{20}, 134
-  \item {\tt eq_assumption}, \bold{50}
+  \item {\tt eq_assume_tac}, \bold{21}, 134
+  \item {\tt eq_assumption}, \bold{51}
   \item {\tt eq_mp_tac}, \bold{142}
   \item {\tt eq_reflection} theorem, \bold{104}, 125
-  \item {\tt eq_thm}, \bold{35}
+  \item {\tt eq_thm}, \bold{36}
   \item {\tt eq_thy}, \bold{60}
-  \item {\tt equal_elim}, \bold{47}
-  \item {\tt equal_intr}, \bold{47}
+  \item {\tt equal_elim}, \bold{48}
+  \item {\tt equal_intr}, \bold{48}
   \item equality, 101--104
-  \item {\tt eres_inst_tac}, \bold{21}
-  \item {\tt eresolve_tac}, \bold{19}
-    \subitem on other than first premise, 43
-  \item {\tt ERROR}, 5
-  \item {\tt error}, 5
-  \item error messages, 5
-  \item {\tt eta_contract}, \bold{5}, 92
-  \item {\tt etac}, \bold{22}
-  \item {\tt EVERY}, \bold{32}
-  \item {\tt EVERY'}, 38
-  \item {\tt EVERY1}, \bold{39}
+  \item {\tt eres_inst_tac}, \bold{22}
+  \item {\tt eresolve_tac}, \bold{20}
+    \subitem on other than first premise, 44
+  \item {\tt ERROR}, 6
+  \item {\tt error}, 6
+  \item error messages, 6
+  \item {\tt eta_contract}, \bold{6}, 92
+  \item {\tt etac}, \bold{23}
+  \item {\tt EVERY}, \bold{33}
+  \item {\tt EVERY'}, 39
+  \item {\tt EVERY1}, \bold{40}
   \item examples
     \subitem of logic definitions, 82
     \subitem of macros, 94, 95
@@ -280,56 +282,56 @@
     \subitem of simplification, 117
     \subitem of translations, 98
   \item exceptions
-    \subitem printing of, 6
-  \item {\tt exit}, \bold{2}
-  \item {\tt extensional}, \bold{48}
+    \subitem printing of, 7
+  \item {\tt exit}, \bold{3}
+  \item {\tt extensional}, \bold{49}
 
   \indexspace
 
-  \item {\tt fa}, \bold{14}
+  \item {\tt fa}, \bold{15}
   \item {\tt Fast_tac}, \bold{142}
   \item {\tt fast_tac}, \bold{140}
-  \item {\tt fd}, \bold{14}
-  \item {\tt fds}, \bold{14}
-  \item {\tt fe}, \bold{14}
-  \item {\tt fes}, \bold{14}
+  \item {\tt fd}, \bold{15}
+  \item {\tt fds}, \bold{15}
+  \item {\tt fe}, \bold{15}
+  \item {\tt fes}, \bold{15}
   \item files
-    \subitem reading, 3, 58
-  \item {\tt filt_resolve_tac}, \bold{28}
-  \item {\tt FILTER}, \bold{33}
-  \item {\tt filter_goal}, \bold{18}
-  \item {\tt filter_thms}, \bold{28}
-  \item {\tt findE}, \bold{11}
-  \item {\tt findEs}, \bold{11}
-  \item {\tt findI}, \bold{11}
-  \item {\tt FIRST}, \bold{32}
-  \item {\tt FIRST'}, 38
-  \item {\tt FIRST1}, \bold{39}
-  \item {\tt FIRSTGOAL}, \bold{37}
-  \item flex-flex constraints, 25, 43, 51
-  \item {\tt flexflex_rule}, \bold{51}
-  \item {\tt flexflex_tac}, \bold{25}
+    \subitem reading, 3, 59
+  \item {\tt filt_resolve_tac}, \bold{29}
+  \item {\tt FILTER}, \bold{34}
+  \item {\tt filter_goal}, \bold{19}
+  \item {\tt filter_thms}, \bold{29}
+  \item {\tt findE}, \bold{12}
+  \item {\tt findEs}, \bold{12}
+  \item {\tt findI}, \bold{12}
+  \item {\tt FIRST}, \bold{33}
+  \item {\tt FIRST'}, 39
+  \item {\tt FIRST1}, \bold{40}
+  \item {\tt FIRSTGOAL}, \bold{38}
+  \item flex-flex constraints, 26, 44, 52
+  \item {\tt flexflex_rule}, \bold{52}
+  \item {\tt flexflex_tac}, \bold{26}
   \item {\tt FOL_basic_ss}, \bold{128}
   \item {\tt FOL_ss}, \bold{128}
-  \item {\tt fold_goals_tac}, \bold{23}
-  \item {\tt fold_tac}, \bold{23}
-  \item {\tt forall_elim}, \bold{49}
-  \item {\tt forall_elim_list}, \bold{49}
-  \item {\tt forall_elim_var}, \bold{49}
-  \item {\tt forall_elim_vars}, \bold{49}
-  \item {\tt forall_intr}, \bold{48}
-  \item {\tt forall_intr_frees}, \bold{49}
-  \item {\tt forall_intr_list}, \bold{49}
-  \item {\tt force_strip_shyps}, \bold{44}
+  \item {\tt fold_goals_tac}, \bold{24}
+  \item {\tt fold_tac}, \bold{24}
+  \item {\tt forall_elim}, \bold{50}
+  \item {\tt forall_elim_list}, \bold{50}
+  \item {\tt forall_elim_var}, \bold{50}
+  \item {\tt forall_elim_vars}, \bold{50}
+  \item {\tt forall_intr}, \bold{49}
+  \item {\tt forall_intr_frees}, \bold{50}
+  \item {\tt forall_intr_list}, \bold{50}
+  \item {\tt force_strip_shyps}, \bold{45}
   \item {\tt Force_tac}, \bold{142}
   \item {\tt force_tac}, \bold{139}
-  \item {\tt forw_inst_tac}, \bold{21}
-  \item forward proof, 20, 41
-  \item {\tt forward_tac}, \bold{20}
-  \item {\tt fr}, \bold{14}
+  \item {\tt forw_inst_tac}, \bold{22}
+  \item forward proof, 21, 42
+  \item {\tt forward_tac}, \bold{21}
+  \item {\tt fr}, \bold{15}
   \item {\tt Free}, \bold{62}, 88
-  \item {\tt freezeT}, \bold{49}
-  \item {\tt frs}, \bold{14}
+  \item {\tt freezeT}, \bold{50}
+  \item {\tt frs}, \bold{15}
   \item {\tt Full_simp_tac}, \bold{105}
   \item {\tt full_simp_tac}, \bold{116}
   \item {\tt full_simplify}, 116
@@ -338,21 +340,22 @@
 
   \indexspace
 
-  \item {\tt get_axiom}, \bold{10}
-  \item {\tt get_thm}, \bold{10}
-  \item {\tt get_thms}, \bold{10}
-  \item {\tt getgoal}, \bold{17}
-  \item {\tt gethyps}, \bold{18}, 37
-  \item {\tt Goal}, \bold{8}, 16
-  \item {\tt goal}, \bold{8}
-  \item {\tt goals_limit}, \bold{12}
-  \item {\tt Goalw}, \bold{8}
-  \item {\tt goalw}, \bold{8}
-  \item {\tt goalw_cterm}, \bold{8}
+  \item {\tt get_axiom}, \bold{11}
+  \item {\tt get_thm}, \bold{11}
+  \item {\tt get_thms}, \bold{11}
+  \item {\tt getenv}, 59
+  \item {\tt getgoal}, \bold{18}
+  \item {\tt gethyps}, \bold{19}, 38
+  \item {\tt Goal}, \bold{9}, 17
+  \item {\tt goal}, \bold{9}
+  \item {\tt goals_limit}, \bold{13}
+  \item {\tt Goalw}, \bold{9}
+  \item {\tt goalw}, \bold{9}
+  \item {\tt goalw_cterm}, \bold{9}
 
   \indexspace
 
-  \item {\tt has_fewer_prems}, \bold{35}
+  \item {\tt has_fewer_prems}, \bold{36}
   \item higher-order pattern, \bold{110}
   \item {\tt HOL_basic_ss}, \bold{109}
   \item {\tt hyp_subst_tac}, \bold{102}
@@ -365,26 +368,26 @@
   \item identifiers, 72
   \item {\tt idt} nonterminal, 92
   \item {\tt idts} nonterminal, \bold{72}, 80
-  \item {\tt IF_UNSOLVED}, \bold{35}
+  \item {\tt IF_UNSOLVED}, \bold{36}
   \item {\tt iff_reflection} theorem, 125
   \item {\tt IFOL_ss}, \bold{128}
   \item {\tt imp_intr} theorem, \bold{104}
-  \item {\tt implies_elim}, \bold{47}
-  \item {\tt implies_elim_list}, \bold{47}
-  \item {\tt implies_intr}, \bold{47}
-  \item {\tt implies_intr_hyps}, \bold{47}
-  \item {\tt implies_intr_list}, \bold{47}
+  \item {\tt implies_elim}, \bold{48}
+  \item {\tt implies_elim_list}, \bold{48}
+  \item {\tt implies_intr}, \bold{48}
+  \item {\tt implies_intr_hyps}, \bold{48}
+  \item {\tt implies_intr_list}, \bold{48}
   \item {\tt incr_boundvars}, \bold{63}, 98
   \item {\tt indexname} ML type, 62, 73
   \item infixes, \bold{79}
   \item {\tt insert} constant, 94
   \item {\tt inst_step_tac}, \bold{141}
-  \item {\tt instance} section, 56
-  \item {\tt instantiate}, \bold{49}
-  \item {\tt instantiate'}, \bold{42}, 49
-  \item instantiation, 21, 42, 49
-  \item {\tt INTLEAVE}, \bold{31}, 33
-  \item {\tt INTLEAVE'}, 38
+  \item {\tt instance} section, 57
+  \item {\tt instantiate}, \bold{50}
+  \item {\tt instantiate'}, \bold{43}, 50
+  \item instantiation, 22, 43, 50
+  \item {\tt INTLEAVE}, \bold{32}, 34
+  \item {\tt INTLEAVE'}, 39
   \item {\tt invoke_oracle}, \bold{66}
   \item {\tt is} nonterminal, 94
 
@@ -394,66 +397,65 @@
 
   \indexspace
 
-  \item {\tt keep_derivs}, \bold{52}
+  \item {\tt keep_derivs}, \bold{53}
 
   \indexspace
 
-  \item $\lambda$-abstractions, 27, \bold{62}
-  \item $\lambda$-calculus, 46, 48, 72
-  \item {\tt lessb}, \bold{27}
+  \item $\lambda$-abstractions, 28, \bold{62}
+  \item $\lambda$-calculus, 47, 49, 72
+  \item {\tt lessb}, \bold{28}
   \item lexer, \bold{72}
-  \item {\tt lift_rule}, \bold{51}
-  \item lifting, 51
-  \item {\tt loadpath}, \bold{58}
+  \item {\tt lift_rule}, \bold{52}
+  \item lifting, 52
   \item {\tt logic} class, 72, 77
   \item {\tt logic} nonterminal, \bold{72}
-  \item {\tt Logic.auto_rename}, \bold{25}
-  \item {\tt Logic.set_rename_prefix}, \bold{24}
-  \item {\tt long_names}, \bold{5}
+  \item {\tt Logic.auto_rename}, \bold{26}
+  \item {\tt Logic.set_rename_prefix}, \bold{25}
+  \item {\tt long_names}, \bold{6}
   \item {\tt loose_bnos}, \bold{63}, 99
 
   \indexspace
 
   \item macros, 90--96
-  \item {\tt make_elim}, \bold{43}, 136
+  \item {\tt make_elim}, \bold{44}, 136
   \item {\tt Match} exception, 97
-  \item {\tt match_tac}, \bold{20}, 134
+  \item {\tt match_tac}, \bold{21}, 134
   \item {\tt max_pri}, 70, \bold{76}
   \item {\tt merge_ss}, \bold{109}
   \item {\tt merge_theories}, \bold{61}
-  \item meta-assumptions, 36, 45, 47, 50
-    \subitem printing of, 4
-  \item meta-equality, 46--48
-  \item meta-implication, 46, 47
-  \item meta-quantifiers, 46, 48
-  \item meta-rewriting, 8, 14, 15, \bold{23}, 
+  \item meta-assumptions, 37, 46, 48, 51
+    \subitem printing of, 5
+  \item meta-equality, 47--49
+  \item meta-implication, 47, 48
+  \item meta-quantifiers, 47, 49
+  \item meta-rewriting, 9, 15, 16, \bold{24}, 
 		\seealso{tactics, theorems}{145}
-    \subitem in theorems, 42
-  \item meta-rules, \see{meta-rules}{1}, 45--51
-  \item {\tt METAHYPS}, 18, \bold{36}
-  \item mixfix declarations, 55, 75--80
+    \subitem in theorems, 43
+  \item meta-rules, \see{meta-rules}{1}, 46--52
+  \item {\tt METAHYPS}, 19, \bold{37}
+  \item mixfix declarations, 56, 75--80
   \item {\tt mk_atomize}, \bold{127}
   \item {\tt mk_simproc}, \bold{123}
   \item {\tt ML} section, 57, 97, 99
   \item model checkers, 81
   \item {\tt mp} theorem, \bold{143}
   \item {\tt mp_tac}, \bold{142}
-  \item {\tt MRL}, \bold{41}
-  \item {\tt MRS}, \bold{41}
+  \item {\tt MRL}, \bold{42}
+  \item {\tt MRS}, \bold{42}
 
   \indexspace
 
   \item name tokens, \bold{72}
   \item {\tt nat_cancel}, \bold{111}
-  \item {\tt net_bimatch_tac}, \bold{27}
-  \item {\tt net_biresolve_tac}, \bold{27}
-  \item {\tt net_match_tac}, \bold{27}
-  \item {\tt net_resolve_tac}, \bold{27}
-  \item {\tt no_tac}, \bold{33}
-  \item {\tt None}, \bold{29}
-  \item {\tt nonterminal} symbols, 55
+  \item {\tt net_bimatch_tac}, \bold{28}
+  \item {\tt net_biresolve_tac}, \bold{28}
+  \item {\tt net_match_tac}, \bold{28}
+  \item {\tt net_resolve_tac}, \bold{28}
+  \item {\tt no_tac}, \bold{34}
+  \item {\tt None}, \bold{30}
+  \item {\tt nonterminal} symbols, 56
   \item {\tt not_elim} theorem, \bold{143}
-  \item {\tt nprems_of}, \bold{44}
+  \item {\tt nprems_of}, \bold{45}
   \item numerals, 72
 
   \indexspace
@@ -461,151 +463,152 @@
   \item {\textit {o}} type, 82
   \item {\tt object}, 66
   \item {\tt op} symbol, 79
-  \item {\tt option} ML type, 29
+  \item {\tt option} ML type, 30
   \item oracles, 66--68
-  \item {\tt ORELSE}, \bold{31}, 33, 37
-  \item {\tt ORELSE'}, 38
+  \item {\tt ORELSE}, \bold{32}, 34, 38
+  \item {\tt ORELSE'}, 39
 
   \indexspace
 
   \item parameters
-    \subitem removing unused, 25
-    \subitem renaming, 14, 24, 51
+    \subitem removing unused, 26
+    \subitem renaming, 15, 25, 52
   \item {\tt parents_of}, \bold{61}
   \item parse trees, 85
   \item {\tt parse_rules}, 92
   \item pattern, higher-order, \bold{110}
-  \item {\tt pause_tac}, \bold{29}
-  \item Poly/{\ML} compiler, 6
-  \item {\tt pop_proof}, \bold{16}
-  \item {\tt pr}, \bold{12}
-  \item {\tt premises}, \bold{8}, 16
-  \item {\tt prems_of}, \bold{44}
+  \item {\tt pause_tac}, \bold{30}
+  \item Poly/{\ML} compiler, 7
+  \item {\tt pop_proof}, \bold{17}
+  \item {\tt pr}, \bold{13}
+  \item {\tt premises}, \bold{9}, 17
+  \item {\tt prems_of}, \bold{45}
   \item {\tt prems_of_ss}, \bold{113}
   \item pretty printing, 76, 78--79, 95
-  \item {\tt Pretty.setdepth}, \bold{4}
-  \item {\tt Pretty.setmargin}, \bold{4}
-  \item {\tt PRIMITIVE}, \bold{28}
+  \item {\tt Pretty.setdepth}, \bold{5}
+  \item {\tt Pretty.setmargin}, \bold{5}
+  \item {\tt PRIMITIVE}, \bold{29}
   \item {\tt primrec}, 107
-  \item {\tt prin}, 6, \bold{17}
-  \item print mode, 55, 99
+  \item {\tt prin}, 7, \bold{18}
+  \item print mode, 56, 99
   \item print modes, 80--81
   \item {\tt print_cs}, \bold{135}
-  \item {\tt print_depth}, \bold{4}
-  \item {\tt print_exn}, \bold{6}, 40
-  \item {\tt print_goals}, \bold{41}
+  \item {\tt print_depth}, \bold{5}
+  \item {\tt print_exn}, \bold{7}, 41
+  \item {\tt print_goals}, \bold{42}
   \item {\tt print_mode}, 80
   \item {\tt print_modes}, 75
   \item {\tt print_rules}, 92
   \item {\tt print_simpset}, \bold{109}
   \item {\tt print_ss}, \bold{108}
   \item {\tt print_syntax}, \bold{61}, \bold{74}
-  \item {\tt print_tac}, \bold{29}
+  \item {\tt print_tac}, \bold{30}
   \item {\tt print_theory}, \bold{61}
-  \item {\tt print_thm}, \bold{41}
-  \item printing control, 3--5
-  \item {\tt printyp}, \bold{17}
+  \item {\tt print_thm}, \bold{42}
+  \item printing control, 4--6
+  \item {\tt printyp}, \bold{18}
   \item priorities, 69, \bold{76}
   \item priority grammars, 69--70
-  \item {\tt prlev}, \bold{12}
-  \item {\tt prlim}, \bold{12}
+  \item {\tt prlev}, \bold{13}
+  \item {\tt prlim}, \bold{13}
   \item productions, 69, 75, 76
     \subitem copy, \bold{75}, 76, 87
-  \item {\tt proof} ML type, 17
-  \item proof objects, 51--53
-  \item proof state, 7
-    \subitem printing of, 12
-  \item {\tt proof_timing}, \bold{13}
-  \item proofs, 7--18
-    \subitem inspecting the state, 17
-    \subitem managing multiple, 16
-    \subitem saving and restoring, 17
-    \subitem stacking, 16
-    \subitem starting, 7
-    \subitem timing, 13
+  \item {\tt proof} ML type, 18
+  \item proof objects, 52--54
+  \item proof state, 8
+    \subitem printing of, 13
+  \item {\tt proof_timing}, \bold{14}
+  \item proofs, 8--19
+    \subitem inspecting the state, 18
+    \subitem managing multiple, 17
+    \subitem saving and restoring, 18
+    \subitem stacking, 17
+    \subitem starting, 8
+    \subitem timing, 14
   \item {\tt PROP} symbol, 71
   \item {\textit {prop}} type, 65, 72
   \item {\tt prop} nonterminal, \bold{70}, 82
-  \item {\tt ProtoPure.thy}, \bold{61}
-  \item {\tt prove_goal}, 13, \bold{15}
-  \item {\tt prove_goalw}, \bold{15}
-  \item {\tt prove_goalw_cterm}, \bold{15}
-  \item {\tt prth}, \bold{40}
-  \item {\tt prthq}, \bold{41}
-  \item {\tt prths}, \bold{41}
-  \item {\tt prune_params_tac}, \bold{25}
+  \item {\tt ProtoPure.thy}, \bold{60}
+  \item {\tt prove_goal}, 14, \bold{16}
+  \item {\tt prove_goalw}, \bold{16}
+  \item {\tt prove_goalw_cterm}, \bold{16}
+  \item {\tt prth}, \bold{41}
+  \item {\tt prthq}, \bold{42}
+  \item {\tt prths}, \bold{42}
+  \item {\tt prune_params_tac}, \bold{26}
   \item {\tt pttrn} nonterminal, \bold{72}
   \item {\tt pttrns} nonterminal, \bold{72}
-  \item {\tt Pure} theory, 54, 70, 74
-  \item {\tt Pure.thy}, \bold{61}
-  \item {\tt push_proof}, \bold{16}
+  \item {\tt Pure} theory, 55, 70, 74
+  \item {\tt Pure.thy}, \bold{60}
+  \item {\tt push_proof}, \bold{17}
   \item {\tt pwd}, \bold{3}
 
   \indexspace
 
-  \item {\tt qed}, \bold{9}, 11
-  \item {\tt qed_goal}, \bold{15}
-  \item {\tt qed_goalw}, \bold{15}
+  \item {\tt qed}, \bold{10}, 12
+  \item {\tt qed_goal}, \bold{16}
+  \item {\tt qed_goalw}, \bold{16}
   \item quantifiers, 80
-  \item {\tt quit}, \bold{2}
+  \item {\tt quit}, \bold{3}
 
   \indexspace
 
-  \item {\tt read}, \bold{17}
+  \item {\tt read}, \bold{18}
   \item {\tt read_axm}, \bold{64}
   \item {\tt read_cterm}, \bold{64}
-  \item {\tt read_instantiate}, \bold{42}
-  \item {\tt read_instantiate_sg}, \bold{42}
+  \item {\tt read_instantiate}, \bold{43}
+  \item {\tt read_instantiate_sg}, \bold{43}
   \item reading
-    \subitem axioms, \see{{\tt assume_ax}}{54}
-    \subitem goals, \see{proofs, starting}{7}
-  \item {\tt reflexive}, \bold{48}
-  \item {\tt ren}, \bold{14}
-  \item {\tt rename_last_tac}, \bold{24}
-  \item {\tt rename_params_rule}, \bold{51}
-  \item {\tt rename_tac}, \bold{24}
+    \subitem axioms, \see{{\tt assume_ax}}{55}
+    \subitem goals, \see{proofs, starting}{8}
+  \item {\tt reflexive}, \bold{49}
+  \item {\tt ren}, \bold{15}
+  \item {\tt rename_last_tac}, \bold{25}
+  \item {\tt rename_params_rule}, \bold{52}
+  \item {\tt rename_tac}, \bold{25}
   \item {\tt rep_cs}, \bold{135}
-  \item {\tt rep_cterm}, \bold{65}
+  \item {\tt rep_cterm}, \bold{64}
   \item {\tt rep_ctyp}, \bold{66}
   \item {\tt rep_ss}, \bold{108}
-  \item {\tt rep_thm}, \bold{44}
-  \item {\tt REPEAT}, \bold{32, 33}
-  \item {\tt REPEAT1}, \bold{32}
-  \item {\tt REPEAT_DETERM}, \bold{32}
-  \item {\tt REPEAT_FIRST}, \bold{38}
-  \item {\tt REPEAT_SOME}, \bold{37}
-  \item {\tt res_inst_tac}, \bold{21}, 25, 26
+  \item {\tt rep_thm}, \bold{45}
+  \item {\tt REPEAT}, \bold{33, 34}
+  \item {\tt REPEAT1}, \bold{33}
+  \item {\tt REPEAT_DETERM}, \bold{33}
+  \item {\tt REPEAT_FIRST}, \bold{39}
+  \item {\tt REPEAT_SOME}, \bold{38}
+  \item {\tt res_inst_tac}, \bold{22}, 26, 27
   \item reserved words, 72, 95
-  \item {\tt reset}, 3
-  \item resolution, 41, 50
-    \subitem tactics, 19
-    \subitem without lifting, 50
-  \item {\tt resolve_tac}, \bold{19}, 134
-  \item {\tt restore_proof}, \bold{17}
-  \item {\tt result}, \bold{9}, 11, 17
+  \item {\tt reset}, 4
+  \item {\tt reset_path}, \bold{60}
+  \item resolution, 42, 51
+    \subitem tactics, 20
+    \subitem without lifting, 51
+  \item {\tt resolve_tac}, \bold{20}, 134
+  \item {\tt restore_proof}, \bold{18}
+  \item {\tt result}, \bold{10}, 12, 18
   \item {\tt rev_mp} theorem, \bold{104}
   \item rewrite rules, 110
     \subitem permutative, 120--123
-  \item {\tt rewrite_goals_rule}, \bold{42}
-  \item {\tt rewrite_goals_tac}, \bold{23}, 42
-  \item {\tt rewrite_rule}, \bold{42}
-  \item {\tt rewrite_tac}, 9, \bold{23}
+  \item {\tt rewrite_goals_rule}, \bold{43}
+  \item {\tt rewrite_goals_tac}, \bold{24}, 43
+  \item {\tt rewrite_rule}, \bold{43}
+  \item {\tt rewrite_tac}, 10, \bold{24}
   \item rewriting
     \subitem object-level, \see{simplification}{1}
     \subitem ordered, 121
     \subitem syntactic, 90--96
-  \item {\tt rewtac}, \bold{22}
-  \item {\tt RL}, \bold{41}
-  \item {\tt RLN}, \bold{41}
-  \item {\tt rotate_prems}, \bold{43}
-  \item {\tt rotate_proof}, \bold{16}
-  \item {\tt rotate_tac}, \bold{25}
-  \item {\tt RS}, \bold{41}
-  \item {\tt RSN}, \bold{41}
-  \item {\tt rtac}, \bold{22}
-  \item {\tt rule_by_tactic}, 25, \bold{43}
+  \item {\tt rewtac}, \bold{23}
+  \item {\tt RL}, \bold{42}
+  \item {\tt RLN}, \bold{42}
+  \item {\tt rotate_prems}, \bold{44}
+  \item {\tt rotate_proof}, \bold{17}
+  \item {\tt rotate_tac}, \bold{26}
+  \item {\tt RS}, \bold{42}
+  \item {\tt RSN}, \bold{42}
+  \item {\tt rtac}, \bold{23}
+  \item {\tt rule_by_tactic}, 26, \bold{44}
   \item rules
-    \subitem converting destruction to elimination, 43
+    \subitem converting destruction to elimination, 44
 
   \indexspace
 
@@ -614,16 +617,16 @@
   \item {\tt safe_step_tac}, 136, \bold{141}
   \item {\tt Safe_tac}, \bold{142}
   \item {\tt safe_tac}, \bold{141}
-  \item {\tt save_proof}, \bold{17}
-  \item saving your work, \bold{1}
-  \item search, 31
-    \subitem tacticals, 33--35
-  \item {\tt SELECT_GOAL}, 23, \bold{36}
-  \item {\tt Seq.seq} ML type, 28
-  \item sequences (lazy lists), \bold{29}
+  \item {\tt save_proof}, \bold{18}
+  \item saving your session, \bold{2}
+  \item search, 32
+    \subitem tacticals, 34--36
+  \item {\tt SELECT_GOAL}, 24, \bold{37}
+  \item {\tt Seq.seq} ML type, 29
+  \item sequences (lazy lists), \bold{30}
   \item sequent calculus, 131
-  \item sessions, 1--6
-  \item {\tt set}, 3
+  \item sessions, 1--7
+  \item {\tt set}, 4
   \item {\tt setloop}, \bold{114}
   \item {\tt setmksimps}, 110, \bold{126}, 128
   \item {\tt setSolver}, \bold{113}, 128
@@ -632,25 +635,26 @@
   \item {\tt settermless}, \bold{121}
   \item {\tt setup}
     \subitem simplifier, 129
-    \subitem theory, 56
+    \subitem theory, 57
   \item shortcuts
-    \subitem for \texttt{by} commands, 13
-    \subitem for tactics, 22
-  \item {\tt show_brackets}, \bold{4}
-  \item {\tt show_consts}, \bold{5}
-  \item {\tt show_hyps}, \bold{4}
-  \item {\tt show_sorts}, \bold{4}, 89, 97
-  \item {\tt show_tags}, \bold{4}
-  \item {\tt show_types}, \bold{4}, 89, 92, 99
-  \item {\tt Sign.certify_term}, \bold{65}
+    \subitem for \texttt{by} commands, 14
+    \subitem for tactics, 23
+  \item {\tt show_brackets}, \bold{5}
+  \item {\tt show_consts}, \bold{6}
+  \item {\tt show_hyps}, \bold{5}
+  \item {\tt show_path}, \bold{59}
+  \item {\tt show_sorts}, \bold{5}, 89, 97
+  \item {\tt show_tags}, \bold{5}
+  \item {\tt show_types}, \bold{5}, 89, 92, 99
+  \item {\tt Sign.certify_term}, \bold{64}
   \item {\tt Sign.certify_typ}, \bold{66}
-  \item {\tt Sign.sg} ML type, 54
-  \item {\tt Sign.stamp_names_of}, \bold{62}
+  \item {\tt Sign.sg} ML type, 55
+  \item {\tt Sign.stamp_names_of}, \bold{61}
   \item {\tt Sign.string_of_term}, \bold{64}
-  \item {\tt Sign.string_of_typ}, \bold{66}
-  \item {\tt sign_of}, 8, 16, \bold{62}
-  \item {\tt sign_of_thm}, \bold{44}
-  \item signatures, \bold{54}, 62, 64, 66
+  \item {\tt Sign.string_of_typ}, \bold{65}
+  \item {\tt sign_of}, 9, 17, \bold{61}
+  \item {\tt sign_of_thm}, \bold{45}
+  \item signatures, \bold{55}, 61, 63, 64, 66
   \item {\tt Simp_tac}, \bold{105}
   \item {\tt simp_tac}, \bold{116}
   \item simplification, 105--129
@@ -676,36 +680,36 @@
   \item {\tt simpset_of}, \bold{109}
   \item {\tt simpset_ref}, \bold{109}
   \item {\tt simpset_ref_of}, \bold{109}
-  \item {\tt size_of_thm}, 34, \bold{35}, 143
+  \item {\tt size_of_thm}, 35, \bold{36}, 143
   \item {\tt sizef}, \bold{143}
   \item {\tt slow_best_tac}, \bold{140}
   \item {\tt slow_step_tac}, 136, \bold{141}
   \item {\tt slow_tac}, \bold{140}
-  \item {\tt SOLVE}, \bold{35}
-  \item {\tt Some}, \bold{29}
-  \item {\tt SOMEGOAL}, \bold{37}
+  \item {\tt SOLVE}, \bold{36}
+  \item {\tt Some}, \bold{30}
+  \item {\tt SOMEGOAL}, \bold{38}
   \item {\tt sort} nonterminal, \bold{72}
   \item sort constraints, 71
-  \item sort hypotheses, 44, 46
+  \item sort hypotheses, 45, 47
   \item sorts
-    \subitem printing of, 4
+    \subitem printing of, 5
   \item {\tt ssubst} theorem, \bold{101}
   \item {\tt stac}, \bold{102}
-  \item stamps, \bold{54}, 62
-  \item {\tt standard}, \bold{43}
+  \item stamps, \bold{55}, 61
+  \item {\tt standard}, \bold{44}
   \item starting up, \bold{1}
   \item {\tt Step_tac}, \bold{142}
   \item {\tt step_tac}, 136, \bold{141}
-  \item {\tt store_thm}, \bold{10}
+  \item {\tt store_thm}, \bold{11}
   \item {\tt string_of_cterm}, \bold{64}
-  \item {\tt string_of_ctyp}, \bold{66}
-  \item {\tt string_of_thm}, \bold{41}
+  \item {\tt string_of_ctyp}, \bold{65}
+  \item {\tt string_of_thm}, \bold{42}
   \item strings, 72
-  \item {\tt SUBGOAL}, \bold{28}
-  \item subgoal module, 7--18
-  \item {\tt subgoal_tac}, \bold{22}
-  \item {\tt subgoals_of_brl}, \bold{26}
-  \item {\tt subgoals_tac}, \bold{23}
+  \item {\tt SUBGOAL}, \bold{29}
+  \item subgoal module, 8--19
+  \item {\tt subgoal_tac}, \bold{23}
+  \item {\tt subgoals_of_brl}, \bold{27}
+  \item {\tt subgoals_tac}, \bold{24}
   \item {\tt subst} theorem, 101, \bold{104}
   \item substitution
     \subitem rules, 101
@@ -714,12 +718,12 @@
   \item {\tt swap_res_tac}, \bold{143}
   \item {\tt swapify}, \bold{143}
   \item {\tt sym} theorem, 102, \bold{104}
-  \item {\tt symmetric}, \bold{48}
+  \item {\tt symmetric}, \bold{49}
   \item {\tt syn_of}, \bold{74}
   \item syntax
     \subitem Pure, 70--75
     \subitem transformations, 85--99
-  \item {\tt syntax} section, 55
+  \item {\tt syntax} section, 56
   \item {\tt Syntax.ast} ML type, 85
   \item {\tt Syntax.mark_boundT}, 99
   \item {\tt Syntax.print_gram}, \bold{74}
@@ -733,118 +737,118 @@
 
   \indexspace
 
-  \item {\tt tactic} ML type, 19
-  \item tacticals, 31--39
-    \subitem conditional, 35
-    \subitem deterministic, 35
-    \subitem for filtering, 33
-    \subitem for restriction to a subgoal, 36
-    \subitem identities for, 32
-    \subitem joining a list of tactics, 32
-    \subitem joining tactic functions, 38
-    \subitem joining two tactics, 31
-    \subitem repetition, 32
-    \subitem scanning for subgoals, 37
-    \subitem searching, 34
-  \item tactics, 19--30
-    \subitem assumption, \bold{20}, 22
-    \subitem commands for applying, 8
-    \subitem debugging, 17
-    \subitem filtering results of, 33
-    \subitem for composition, 26
+  \item {\tt tactic} ML type, 20
+  \item tacticals, 32--40
+    \subitem conditional, 36
+    \subitem deterministic, 36
+    \subitem for filtering, 34
+    \subitem for restriction to a subgoal, 37
+    \subitem identities for, 33
+    \subitem joining a list of tactics, 33
+    \subitem joining tactic functions, 39
+    \subitem joining two tactics, 32
+    \subitem repetition, 33
+    \subitem scanning for subgoals, 38
+    \subitem searching, 35
+  \item tactics, 20--31
+    \subitem assumption, \bold{21}, 23
+    \subitem commands for applying, 9
+    \subitem debugging, 18
+    \subitem filtering results of, 34
+    \subitem for composition, 27
     \subitem for contradiction, 142
-    \subitem for inserting facts, 22
+    \subitem for inserting facts, 23
     \subitem for Modus Ponens, 142
-    \subitem instantiation, 21
-    \subitem matching, 20
-    \subitem meta-rewriting, 22, \bold{23}
-    \subitem primitives for coding, 28
-    \subitem resolution, \bold{19}, 22, 26, 27
-    \subitem restricting to a subgoal, 36
+    \subitem instantiation, 22
+    \subitem matching, 21
+    \subitem meta-rewriting, 23, \bold{24}
+    \subitem primitives for coding, 29
+    \subitem resolution, \bold{20}, 23, 27, 28
+    \subitem restricting to a subgoal, 37
     \subitem simplification, 115
     \subitem substitution, 101--104
-    \subitem tracing, 29
+    \subitem tracing, 30
   \item {\tt TERM}, 64
   \item {\tt term} ML type, 62, 88
   \item terms, \bold{62}
-    \subitem certified, \bold{64}
+    \subitem certified, \bold{63}
     \subitem made from ASTs, 88
-    \subitem printing of, 17, 64
-    \subitem reading of, 17
+    \subitem printing of, 18, 64
+    \subitem reading of, 18
   \item {\tt TFree}, \bold{65}
-  \item {\tt THEN}, \bold{31}, 33, 37
-  \item {\tt THEN'}, 38
-  \item {\tt THEN_BEST_FIRST}, \bold{34}
-  \item theorems, 40--53
-    \subitem equality of, 35
-    \subitem extracting, 10
-    \subitem extracting proved, 9
-    \subitem joining by resolution, 41
-    \subitem of pure theory, 24
-    \subitem printing of, 40
-    \subitem retrieving, 11
-    \subitem size of, 35
-    \subitem standardizing, 43
-    \subitem storing, 10
-    \subitem taking apart, 43
-  \item theories, 54--68
-    \subitem axioms of, 10
-    \subitem constructing, \bold{61}
+  \item {\tt the_context}, \bold{4}
+  \item {\tt THEN}, \bold{32}, 34, 38
+  \item {\tt THEN'}, 39
+  \item {\tt THEN_BEST_FIRST}, \bold{35}
+  \item theorems, 41--54
+    \subitem equality of, 36
+    \subitem extracting, 11
+    \subitem extracting proved, 10
+    \subitem joining by resolution, 42
+    \subitem of pure theory, 25
+    \subitem printing of, 41
+    \subitem retrieving, 12
+    \subitem size of, 36
+    \subitem standardizing, 44
+    \subitem storing, 11
+    \subitem taking apart, 44
+  \item theories, 55--68
+    \subitem axioms of, 11
+    \subitem constructing, \bold{60}
     \subitem inspecting, \bold{61}
-    \subitem loading, 58
-    \subitem parent, \bold{54}
-    \subitem pseudo, \bold{59}
-    \subitem reloading, \bold{59}
-    \subitem removing, \bold{59}
-    \subitem theorems of, 10
-  \item {\tt THEORY} exception, 10, 54
-  \item {\tt theory} ML type, 54
+    \subitem parent, \bold{55}
+    \subitem reading, 3, 59
+    \subitem theorems of, 11
+  \item {\tt THEORY} exception, 11, 55
+  \item {\tt theory}, \bold{4}
+  \item {\tt theory} ML type, 55
   \item {\tt Theory.add_oracle}, \bold{66}
-  \item {\tt theory_of_thm}, \bold{44}
+  \item {\tt theory_of_thm}, \bold{45}
   \item {\tt thin_refl} theorem, \bold{104}
-  \item {\tt thin_tac}, \bold{25}
-  \item {\tt THM} exception, 40, 41, 45, 50
-  \item {\tt thm}, \bold{10}
-  \item {\tt thm} ML type, 40
-  \item {\tt thms}, \bold{10}
-  \item {\tt thms_containing}, \bold{11}
-  \item {\tt thms_of}, \bold{10}
+  \item {\tt thin_tac}, \bold{26}
+  \item {\tt THM} exception, 41, 42, 46, 51
+  \item {\tt thm}, \bold{11}
+  \item {\tt thm} ML type, 41
+  \item {\tt thms}, \bold{11}
+  \item {\tt thms_containing}, \bold{12}
+  \item {\tt thms_of}, \bold{11}
   \item {\tt tid} nonterminal, \bold{72}, 86, 93
   \item {\tt time_use}, \bold{3}
-  \item {\tt time_use_thy}, \bold{58}
-  \item timing statistics, 13
-  \item {\tt toggle}, 3
+  \item {\tt time_use_thy}, \bold{4}
+  \item timing statistics, 14
+  \item {\tt toggle}, 4
   \item token class, 99
   \item token translations, 99--100
   \item token_translation, 100
   \item {\tt token_translation}, 100
-  \item {\tt topthm}, \bold{17}
-  \item {\tt tpairs_of}, \bold{44}
-  \item {\tt trace_BEST_FIRST}, \bold{34}
-  \item {\tt trace_DEPTH_FIRST}, \bold{34}
-  \item {\tt trace_goalno_tac}, \bold{38}
-  \item {\tt trace_REPEAT}, \bold{32}
+  \item {\tt topthm}, \bold{18}
+  \item {\tt touch_thy}, \bold{59}
+  \item {\tt tpairs_of}, \bold{45}
+  \item {\tt trace_BEST_FIRST}, \bold{35}
+  \item {\tt trace_DEPTH_FIRST}, \bold{35}
+  \item {\tt trace_goalno_tac}, \bold{39}
+  \item {\tt trace_REPEAT}, \bold{33}
   \item {\tt trace_simp}, \bold{106}, 118
   \item tracing
     \subitem of classical prover, 139
     \subitem of macros, 94
-    \subitem of searching tacticals, 34
+    \subitem of searching tacticals, 35
     \subitem of simplification, 107, 118--119
-    \subitem of tactics, 29
-    \subitem of unification, 45
+    \subitem of tactics, 30
+    \subitem of unification, 46
   \item {\tt transfer}, \bold{60}
   \item {\tt transfer_sg}, \bold{60}
-  \item {\tt transitive}, \bold{48}
+  \item {\tt transitive}, \bold{49}
   \item translations, 96--99
     \subitem parse, 80, 88
     \subitem parse AST, \bold{86}, 87
     \subitem print, 80
     \subitem print AST, \bold{89}
   \item {\tt translations} section, 91
-  \item {\tt trivial}, \bold{51}
+  \item {\tt trivial}, \bold{52}
   \item {\tt Trueprop} constant, 82
-  \item {\tt TRY}, \bold{32, 33}
-  \item {\tt TRYALL}, \bold{37}
+  \item {\tt TRY}, \bold{33, 34}
+  \item {\tt TRYALL}, \bold{38}
   \item {\tt TVar}, \bold{65}
   \item {\tt tvar} nonterminal, \bold{72, 73}, 86, 93
   \item {\tt typ} ML type, 65
@@ -854,23 +858,23 @@
   \item type constraints, 72, 80, 89
   \item type constructors, \bold{65}
   \item type identifiers, 72
-  \item type synonyms, \bold{55}
+  \item type synonyms, \bold{56}
   \item type unknowns, \bold{65}, 72
-    \subitem freezing/thawing of, 49
+    \subitem freezing/thawing of, 50
   \item type variables, \bold{65}
   \item types, \bold{65}
     \subitem certified, \bold{65}
-    \subitem printing of, 4, 17, 65
+    \subitem printing of, 5, 18, 65
 
   \indexspace
 
-  \item {\tt undo}, 7, \bold{12}, 16
+  \item {\tt undo}, 8, \bold{13}, 17
   \item unknowns, \bold{62}, 72
-  \item {\tt unlink_thy}, \bold{59}
-  \item {\tt update}, \bold{59}
-  \item {\tt uresult}, \bold{9}, 11, 17
+  \item {\tt update_thy}, \bold{59}
+  \item {\tt uresult}, \bold{10}, 12, 18
   \item {\tt use}, \bold{3}
-  \item {\tt use_thy}, \bold{58}
+  \item {\tt use_thy}, \bold{4}
+  \item {\tt use_thy_only}, \bold{59}
 
   \indexspace
 
@@ -881,13 +885,13 @@
     \subitem bound, \bold{62}
     \subitem free, \bold{62}
   \item {\tt variant_abs}, \bold{63}
-  \item {\tt varifyT}, \bold{49}
+  \item {\tt varifyT}, \bold{50}
 
   \indexspace
 
-  \item {\tt warning}, 5
-  \item warnings, 5
-  \item {\tt writeln}, 5
+  \item {\tt warning}, 6
+  \item warnings, 6
+  \item {\tt writeln}, 6
 
   \indexspace
 
@@ -896,6 +900,6 @@
 
   \indexspace
 
-  \item {\tt zero_var_indexes}, \bold{43}
+  \item {\tt zero_var_indexes}, \bold{44}
 
 \end{theindex}

--- a/doc-src/Ref/ref.tex	Mon May 03 14:43:52 1999 +0200
+++ b/doc-src/Ref/ref.tex	Mon May 03 18:35:48 1999 +0200
@@ -2,7 +2,7 @@
 \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
 
 %% $Id$
-%%\includeonly{}
+%\includeonly{introduction}
 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
 %%% to delete old ones:  \\indexbold{\*[^}]*}
 %% run    sedindex ref    to prepare index file

--- a/doc-src/Ref/theories.tex	Mon May 03 14:43:52 1999 +0200
+++ b/doc-src/Ref/theories.tex	Mon May 03 18:35:48 1999 +0200
@@ -33,16 +33,12 @@
 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
 definitions; here is an explanation of the constituent parts:
 \begin{description}
-\item[{\it theoryDef}] is the full definition.  The new theory is
-  called $id$.  It is the union of the named {\bf parent
+\item[{\it theoryDef}] is the full definition.  The new theory is called $id$.
+  It is the union of the named {\bf parent
     theories}\indexbold{theories!parent}, possibly extended with new
-  components.  \thydx{Pure} and \thydx{CPure} are the basic theories,
-  which contain only the meta-logic.  They differ just in their
-  concrete syntax for function applications.
-
-  Normally each {\it name\/} is an identifier, the name of the parent theory.
-  Quoted strings can be used to document additional file dependencies; see
-  \S\ref{LoadingTheories} for details.
+  components.  \thydx{Pure} and \thydx{CPure} are the basic theories, which
+  contain only the meta-logic.  They differ just in their concrete syntax for
+  function applications.
 
 \item[$classes$]
   is a series of class declarations.  Declaring {\tt$id$ < $id@1$ \dots\
@@ -231,143 +227,75 @@
 \end{itemize}
 
 
-\section{Loading a new theory}\label{LoadingTheories}
-\index{theories!loading}\index{files!reading}
+\section{The theory loader}\label{sec:more-theories}
+\index{theories!reading}\index{files!reading}
+
+Isabelle's theory loader manages dependencies of the internal graph of theory
+nodes (the \emph{theory database}) and the external view of the file system.
+See \S\ref{sec:intro-theories} for its most basic commands, such as
+\texttt{use_thy}.  There are a few more operations available.
+
 \begin{ttbox}
-use_thy         : string -> unit
-time_use_thy    : string -> unit
-loadpath        : string list ref \hfill{\bf initially {\tt["."]}}
+use_thy_only    : string -> unit
+update_thy      : string -> unit
+touch_thy       : string -> unit
 delete_tmpfiles : bool ref \hfill{\bf initially true}
 \end{ttbox}
 
 \begin{ttdescription}
-\item[\ttindexbold{use_thy} $thyname$]
-  reads the theory $thyname$ and creates an \ML{} structure as described below.
-
-\item[\ttindexbold{time_use_thy} $thyname$]
-  calls {\tt use_thy} $thyname$ and reports the time taken.
-
-\item[\ttindexbold{loadpath}]
-  contains a list of directories to search when locating the files that
-  define a theory.  This list is only used if the theory name in {\tt
-    use_thy} does not specify the path explicitly.
-
-\item[reset \ttindexbold{delete_tmpfiles};]
-suppresses the deletion of temporary files.
+\item[\ttindexbold{use_thy_only} $name$;] is similar to \texttt{use_thy}, but
+  processes the actual theory file $name$\texttt{.thy} only, ignoring
+  $name$\texttt{.ML}.  This might be useful in replaying proof scripts by hand
+  from the very beginning, starting with the fresh theory.
+  
+\item[\ttindexbold{update_thy} $name$;] is similar to \texttt{use_thy}, but
+  ensures that theory $name$ is fully up-to-date with respect to the file
+  system --- apart from $name$ itself its parents may be reloaded as well.
+  
+\item[\ttindexbold{touch_thy} $name$;] marks theory node $name$ of the
+  internal graph as outdated.  While the theory remains usable, subsequent
+  operations such as \texttt{use_thy} may cause a reload.
+  
+\item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually
+  involves temporary {\ML} files to be created.  By default, these are deleted
+  afterwards.  Resetting the \texttt{delete_tmpfiles} flag inhibits this,
+  leaving the generated code for debugging purposes.  The basic location for
+  temporary files is determined by the \texttt{ISABELLE_TMP} environment
+  variable, which is private to the running Isabelle process (it may be
+  retrieved by \ttindex{getenv} from {\ML}).
 \end{ttdescription}
-%
-Each theory definition must reside in a separate file.  Let the file
-{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose
-parent theories are $TB@1$ \dots $TB@n$.  Calling
-\texttt{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy},
-writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the
-latter file.  Recursive {\tt use_thy} calls load those parent theories
-that have not been loaded previously; the recursive calls may continue
-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 and no errors occurred.
 
-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.
+\medskip Theory and {\ML} files are located by skimming through the
+directories listed in Isabelle's internal load path, which merely contains the
+current directory ``\texttt{.}'' by default.  The load path may be accessed by
+the following operations.
 
-Some applications construct theories directly by calling \ML\ functions.  In
-this situation there is no {\tt.thy} file, only an {\tt.ML} file.  The
-{\tt.ML} file must declare an \ML\ structure having the theory's name and a
-component {\tt thy} containing the new theory object.
-Section~\ref{sec:pseudo-theories} below describes a way of linking such
-theories to their parents.
-
-
-\section{Reloading modified theories}\label{sec:reloading-theories}
-\indexbold{theories!reloading}
 \begin{ttbox}
-update     : unit -> unit
-unlink_thy : string -> unit
+show_path: unit -> string list
+add_path: string -> unit
+del_path: string -> unit
+reset_path: unit -> unit
 \end{ttbox}
-Changing a theory on disk often makes it necessary to reload all theories
-descended from it.  However, {\tt use_thy} reads only one theory, even if
-some of the parent theories are out of date.  In this case you should call
-{\tt update()}.
-
-Isabelle keeps track of all loaded theories and their files.  If
-\texttt{use_thy} finds that the theory to be loaded has been read
-before, it determines whether to reload the theory as follows.  First
-it looks for the theory's files in their previous location.  If it
-finds them, it compares their modification times to the internal data
-and stops if they are equal.  If the files have been moved, {\tt
-  use_thy} searches for them as it would for a new theory.  After {\tt
-  use_thy} reloads a theory, it marks the children as out-of-date.
 
 \begin{ttdescription}
-\item[\ttindexbold{update}()]
-  reloads all modified theories and their descendants in the correct order.
-
-\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
-  informs Isabelle that theory $thyname$ no longer exists.  If you delete the
-  theory files for $thyname$ then you must execute {\tt unlink_thy};
-  otherwise {\tt update} will complain about a missing file.
+\item[\ttindexbold{show_path}();] displays the load path components in
+  canonical string representation, which is always according to Unix rules.
+  
+\item[\ttindexbold{add_path} $dir$;] adds component $dir$ to the beginning of
+  the load path.
+  
+\item[\ttindexbold{del_path} $dir$;] removes any occurrences of component
+  $dir$ from the load path.
+  
+\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
+  (current directory) only.
 \end{ttdescription}
 
-
-\subsection{*Pseudo theories}\label{sec:pseudo-theories}
-\indexbold{theories!pseudo}%
-Any automatic reloading facility requires complete knowledge of all
-dependencies.  Sometimes theories depend on objects created in \ML{} files
-with no associated theory definition file.  These objects may be theories but
-they could also be theorems, proof procedures, etc.
-
-Unless such dependencies are documented, {\tt update} fails to reload these
-\ML{} files and the system is left in a state where some objects, such as
-theorems, still refer to old versions of theories.  This may lead to the
-error
-\begin{ttbox}
-Attempt to merge different versions of theories: \dots
-\end{ttbox}
-Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
-those not associated with a theory definition.
-
-Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
-theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
-theorems proved in {\tt orphan.ML}.  Then {\tt B.thy} should
-mention this dependency as follows:
-\begin{ttbox}
-B = \(\ldots\) + "orphan" + \(\ldots\)
-\end{ttbox}
-Quoted strings stand for theories which have to be loaded before the
-current theory is read but which are not used in building the base of
-theory~$B$.  Whenever {\tt orphan} changes and is reloaded, Isabelle
-knows that $B$ has to be updated, too.
-
-Note that it's necessary for {\tt orphan} to declare a special ML
-object of type {\tt theory} which is present in all theories.  This is
-normally achieved by adding the file {\tt orphan.thy} to make {\tt
-orphan} a {\bf pseudo theory}.  A minimum version of {\tt orphan.thy}
-would be
-
-\begin{ttbox}
-orphan = Pure
-\end{ttbox}
-
-which uses {\tt Pure} to make a dummy theory.  Normally though the
-orphaned file has its own dependencies.  If {\tt orphan.ML} depends on
-theories or files $A@1$, \ldots, $A@n$, record this by creating the
-pseudo theory in the following way:
-\begin{ttbox}
-orphan = \(A@1\) + \(\ldots\) + \(A@n\)
-\end{ttbox}
-The resulting theory ensures that {\tt update} reloads {\tt orphan}
-whenever it reloads one of the $A@i$.
-
-For an extensive example of how this technique can be used to link
-lots of theory files and load them by just a few {\tt use_thy} calls
-see the sources of one of the major object-logics (e.g.\ \ZF).
-
+In operations referring indirectly to some file, such as
+\texttt{use_thy}~$name$, the argument may be prefixed by some directory that
+will be used as temporary load path.  Note that, depending on which parts of
+the ancestry of $name$ are already loaded, the dynamic change of paths might
+be hard to predict.  Use this feature with care only.
 
 
 \section{Basic operations on theories}\label{BasicOperationsOnTheories}