--- 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