diff -r fbf60999dc31 -r 75d8778f94d3 doc-src/Logics/preface.tex
--- a/doc-src/Logics/preface.tex	Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-\chapter*{Preface}
-Several logics come with Isabelle.  Many of them are sufficiently developed
-to serve as comfortable reasoning environments.  They are also good
-starting points for defining new logics.  Each logic is distributed with
-sample proofs, some of which are described in this document.
-
-\texttt{HOL} is currently the best developed Isabelle object-logic, including
-an extensive library of (concrete) mathematics, and various packages for
-advanced definitional concepts (like (co-)inductive sets and types,
-well-founded recursion etc.). The distribution also includes some large
-applications.  See the separate manual \emph{Isabelle's Logics: HOL}.  There
-is also a comprehensive tutorial on Isabelle/HOL available.
-
-\texttt{ZF} provides another starting point for applications, with a slightly
-less developed library than \texttt{HOL}.  \texttt{ZF}'s definitional packages
-are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides
-more advanced constructions for sets than simply-typed \texttt{HOL}.
-\texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
-in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.
-
-\medskip There are some further logics distributed with Isabelle:
-\begin{ttdescription}
-\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
-  which is the basis of a preliminary method for deriving programs from
-  proofs~\cite{coen92}.  It is built upon classical~FOL.
- 
-\item[\thydx{LCF}] is a version of Scott's Logic for Computable
-  Functions, which is also implemented by the~{\sc lcf}
-  system~\cite{paulson87}.  It is built upon classical~FOL.
-  
-\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
-  \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.
- 
-\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
-Theory~\cite{nordstrom90}, with extensional equality.  Universes are not
-included.
-
-\item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
- \end{ttdescription}
-
-The directory \texttt{Sequents} contains several logics based
-  upon the sequent calculus.  Sequents have the form $A@1,\ldots,A@m\turn
-B@1,\ldots,B@n$; rules are applied using associative matching.
-\begin{ttdescription}
-\item[\thydx{LK}] is classical first-order logic as a sequent calculus.
-
-\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.  
-
-\item[\thydx{ILL}] implements intuitionistic linear logic.
-\end{ttdescription}
-
-The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt
-  Cube} are undocumented.  All object-logics' sources are distributed with
-Isabelle (see the directory \texttt{src}).  They are also available for
-browsing on the WWW at
-
-\begin{center}\small
-  \begin{tabular}{l}
-    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
-    \url{http://isabelle.in.tum.de/library/} \\
-  \end{tabular}
-\end{center}
-
-Note that this is not necessarily consistent with your local sources!
-
-\medskip Do not read the \emph{Isabelle's Logics} manuals before reading
-\emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and
-performing some Isabelle proofs.  Consult the {\em Reference Manual} for more
-information on tactics, packages, etc.
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "logics"
-%%% End: