doc-src/Intro/getting.tex
 changeset 1878 ac8e534b4834 parent 331 13660d5f6a77 child 3103 98af809fee46
--- 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.

`