--- a/doc-src/Intro/foundations.tex Mon Jul 22 16:15:45 1996 +0200
+++ b/doc-src/Intro/foundations.tex Mon Jul 22 16:16:51 1996 +0200
@@ -264,7 +264,7 @@
\index{meta-equality|bold}
Object-logics are formalized by extending Isabelle's
-meta-logic~\cite{paulson89}, which is intuitionistic higher-order logic.
+meta-logic~\cite{paulson-found}, which is intuitionistic higher-order logic.
The meta-level connectives are {\bf implication}, the {\bf universal
quantifier}, and {\bf equality}.
\begin{itemize}
@@ -367,7 +367,7 @@
\begin{warn}
Earlier versions of Isabelle, and certain
-papers~\cite{paulson89,paulson700}, use $\List{P}$ to mean $Trueprop(P)$.
+papers~\cite{paulson-found,paulson700}, use $\List{P}$ to mean $Trueprop(P)$.
\end{warn}
\subsection{Quantifier rules and substitution}
@@ -477,7 +477,7 @@
\section{Proof construction in Isabelle}
I have elsewhere described the meta-logic and demonstrated it by
-formalizing first-order logic~\cite{paulson89}. There is a one-to-one
+formalizing first-order logic~\cite{paulson-found}. There is a one-to-one
correspondence between meta-level proofs and object-level proofs. To each
use of a meta-level axiom, such as $(\forall I)$, there is a use of the
corresponding object-level rule. Object-level assumptions and parameters
@@ -759,7 +759,7 @@
\[ \vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} }
\quad\hbox{provided $x$, $y$ not free in the assumptions}
\]
-I discuss lifting and parameters at length elsewhere~\cite{paulson89}.
+I discuss lifting and parameters at length elsewhere~\cite{paulson-found}.
Miller goes into even greater detail~\cite{miller-mixed}.
@@ -843,7 +843,7 @@
with $\lambda x@1 \ldots x@l. \theta$. Isabelle supplies the parameters
$x@1$,~\ldots,~$x@l$ to higher-order unification as bound variables, which
regards them as unique constants with a limited scope --- this enforces
-parameter provisos~\cite{paulson89}.
+parameter provisos~\cite{paulson-found}.
The premise represents a proof state with~$n$ subgoals, of which the~$i$th
is to be solved by assumption. Isabelle searches the subgoal's context for
--- a/doc-src/Intro/getting.tex Mon Jul 22 16:15:45 1996 +0200
+++ b/doc-src/Intro/getting.tex Mon Jul 22 16:16:51 1996 +0200
@@ -591,7 +591,7 @@
Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an
attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former
proof succeeds, and the latter fails, because of the scope of quantified
-variables~\cite{paulson89}. Unification helps even in these trivial
+variables~\cite{paulson-found}. Unification helps even in these trivial
proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$,
but we need never say so. This choice is forced by the reflexive law for
equality, and happens automatically.
@@ -668,7 +668,7 @@
\end{ttbox}
There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
first-order logic. I have elsewhere proved the faithfulness of Isabelle's
-encoding of first-order logic~\cite{paulson89}; there could, of course, be
+encoding of first-order logic~\cite{paulson-found}; there could, of course, be
faults in the implementation.
--- a/doc-src/Intro/intro.bbl Mon Jul 22 16:15:45 1996 +0200
+++ b/doc-src/Intro/intro.bbl Mon Jul 22 16:16:51 1996 +0200
@@ -14,8 +14,7 @@
\bibitem{mgordon79}
Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.
\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.
-\newblock Springer, 1979.
-\newblock LNCS 78.
+\newblock LNCS 78. Springer, 1979.
\bibitem{haskell-tutorial}
Paul Hudak and Joseph~H. Fasel.
@@ -49,7 +48,7 @@
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
\newblock Oxford University Press, 1990.
-\bibitem{paulson86}
+\bibitem{paulson-natural}
Lawrence~C. Paulson.
\newblock Natural deduction as higher-order resolution.
\newblock {\em Journal of Logic Programming}, 3:237--258, 1986.
@@ -59,7 +58,7 @@
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
\newblock Cambridge University Press, 1987.
-\bibitem{paulson89}
+\bibitem{paulson-found}
Lawrence~C. Paulson.
\newblock The foundation of a generic theorem prover.
\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989.
--- a/doc-src/Intro/intro.tex Mon Jul 22 16:15:45 1996 +0200
+++ b/doc-src/Intro/intro.tex Mon Jul 22 16:16:51 1996 +0200
@@ -36,10 +36,10 @@
\pagestyle{headings}
\part*{Preface}
-\index{Isabelle!overview}
-\index{Isabelle!object-logics supported}
-Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.
-It has been instantiated to support reasoning in several object-logics:
+\index{Isabelle!overview} \index{Isabelle!object-logics supported}
+Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem
+prover. It has been instantiated to support reasoning in several
+object-logics:
\begin{itemize}
\item first-order logic, constructive and classical versions
\item higher-order logic, similar to that of Gordon's {\sc