doc-src/Ref/introduction.tex

 by their operands (subgoals, tactics, theorems), and by their usefulness.
 In each section, basic functions appear first, then advanced functions, and
 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
 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.
-
-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.
+This should start an interactive \ML{} session with the default object-logic
+(usually {\HOL}) already pre-loaded.
+
+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.
 \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).
-
-\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:
-\begin{ttbox}
-isabelle FOL Foo
+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 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 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 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.
-
-\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 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.
+
+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 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}
 \begin{ttbox} 
 quit    : unit -> unit

 
 The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
 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}
 \begin{ttbox}
 set     : bool ref -> bool

 
 \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.
+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
 \texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
 typical warning would look like this: