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 @@
 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.