diff r cd41a57221d0 r 1f5a94209c97 docsrc/Intro/intro.tex
 a/docsrc/Intro/intro.tex Mon May 02 12:34:56 1994 +0200
+++ b/docsrc/Intro/intro.tex Tue May 03 10:40:24 1994 +0200
@@ 43,7 +43,7 @@
\begin{itemize}
\item firstorder logic, constructive and classical versions
\item higherorder logic, similar to that of Gordon's {\sc
hol}~\cite{gordon88a}
+hol}~\cite{mgordonhol}
\item ZermeloFraenkel set theory~\cite{suppes72}
\item an extensional version of MartinL\"of's Type Theory~\cite{nordstrom90}
\item the classical firstorder sequent calculus, {\sc lk}
@@ 68,7 +68,7 @@
texts~\cite{galton90,reeves90}.
\index{LCF}
{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an
+{\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows
ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
abstract type; tactics and tacticals support backward proof. But {\sc lcf}
@@ 76,15 +76,6 @@
by terms. You may find my other writings~\cite{paulson87,paulsonhandbook}
helpful in understanding the relationship between {\sc lcf} and Isabelle.
Isabelle does not keep a record of inference steps. Each step is checked
at run time to ensure that theorems can only be constructed by applying
inference rules. An Isabelle proof typically involves hundreds of
primitive inferences, and would be unintelligible if displayed.
Discarding proofs saves vast amounts of storage. But can Isabelle be
trusted? If desired, objectlogics can be formalized such that each
theorem carries a proof term, which could be checked by another program.
Proofs can also be traced.

\index{Isabelle!release history} Isabelle was first distributed in 1986.
The 1987 version introduced a higherorder metalogic with an improved
treatment of quantifiers. The 1988 version added limited polymorphism and
@@ 142,7 +133,7 @@
\include{advanced}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{string,atp,funprog,general,logicprog,theory}
+\bibliography{string,atp,funprog,general,logicprog,isabelle,theory}
\input{intro.ind}
\end{document}