doc-src/Logics/preface.tex
changeset 9695 ec7d7f877712
parent 6627 c2511c9ea37e
child 42637 381fdcab0f36
     1.1 --- a/doc-src/Logics/preface.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/Logics/preface.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -23,11 +23,11 @@
     1.4  \begin{ttdescription}
     1.5  \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
     1.6    which is the basis of a preliminary method for deriving programs from
     1.7 -  proofs~\cite{coen92}.  It is built upon classical~\FOL{}.
     1.8 +  proofs~\cite{coen92}.  It is built upon classical~FOL.
     1.9   
    1.10  \item[\thydx{LCF}] is a version of Scott's Logic for Computable
    1.11    Functions, which is also implemented by the~{\sc lcf}
    1.12 -  system~\cite{paulson87}.  It is built upon classical~\FOL{}.
    1.13 +  system~\cite{paulson87}.  It is built upon classical~FOL.
    1.14    
    1.15  \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
    1.16    \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.