1.1 --- a/doc-src/Logics/preface.tex Tue May 04 18:04:45 1999 +0200
1.2 +++ b/doc-src/Logics/preface.tex Tue May 04 18:05:34 1999 +0200
1.3 @@ -5,10 +5,21 @@
1.4 starting points for defining new logics. Each logic is distributed with
1.5 sample proofs, some of which are described in this document.
1.6
1.7 -The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set
1.8 -theory) are described in a separate manual~\cite{isabelle-ZF}. Here are the
1.9 -others:
1.10 +\texttt{HOL} is currently the best developed Isabelle object-logic, including
1.11 +an extensive library of (concrete) mathematics, and various packages for
1.12 +advanced definitional concepts (like (co-)inductive sets and types,
1.13 +well-founded recursion etc.). The distribution also includes some large
1.14 +applications. See the separate manual \emph{Isabelle's Logics: HOL}. There
1.15 +is also a comprehensive tutorial on Isabelle/HOL available.
1.16
1.17 +\texttt{ZF} provides another starting point for applications, with a slightly
1.18 +less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages
1.19 +are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides
1.20 +more advanced constructions for sets than simply-typed \texttt{HOL}.
1.21 +\texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
1.22 +in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.
1.23 +
1.24 +\medskip There are some further logics distributed with Isabelle:
1.25 \begin{ttdescription}
1.26 \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
1.27 which is the basis of a preliminary method for deriving programs from
1.28 @@ -17,14 +28,9 @@
1.29 \item[\thydx{LCF}] is a version of Scott's Logic for Computable
1.30 Functions, which is also implemented by the~{\sc lcf}
1.31 system~\cite{paulson87}. It is built upon classical~\FOL{}.
1.32 -
1.33 -\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
1.34 -which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
1.35 -This object-logic should not be confused with Isabelle's meta-logic, which is
1.36 -also a form of higher-order logic.
1.37 -
1.38 -\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an
1.39 - extension of \texttt{HOL}\@.
1.40 +
1.41 +\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
1.42 + \texttt{HOL}\@. %FIXME See \cite{MNOS98} for more details on \texttt{HOLCF}.
1.43
1.44 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
1.45 Theory~\cite{nordstrom90}, with extensional equality. Universes are not
1.46 @@ -44,19 +50,20 @@
1.47 \item[\thydx{ILL}] implements intuitionistic linear logic.
1.48 \end{ttdescription}
1.49
1.50 -The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt
1.51 - Cube} are undocumented. All object-logics' sources are
1.52 -distributed with Isabelle (see the directory \texttt{src}). They are
1.53 -also available for browsing on the WWW at
1.54 +The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt
1.55 + Cube} are undocumented. All object-logics' sources are distributed with
1.56 +Isabelle (see the directory \texttt{src}). They are also available for
1.57 +browsing on the WWW at
1.58 \begin{ttbox}
1.59 http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/
1.60 http://isabelle.in.tum.de/library/
1.61 \end{ttbox}
1.62 Note that this is not necessarily consistent with your local sources!
1.63
1.64 -\medskip Do not read this manual before reading \emph{Introduction to
1.65 - Isabelle} and performing some Isabelle proofs. Consult the {\em Reference
1.66 - Manual} for more information on tactics, packages, etc.
1.67 +\medskip Do not read the \emph{Isabelle's Logics} manuals before reading
1.68 +\emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and
1.69 +performing some Isabelle proofs. Consult the {\em Reference Manual} for more
1.70 +information on tactics, packages, etc.
1.71
1.72
1.73 %%% Local Variables: