# HG changeset patch
# User paulson
# Date 838045011 -7200
# Node ID ac8e534b48341fdb08ca75d752bde0d2cbad4e5b
# Parent  3063f6b7a189c455dba483cbe0a1a6da07859e31
Updated BibTeX identifiers

diff -r 3063f6b7a189 -r ac8e534b4834 doc-src/Intro/foundations.tex
--- 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
diff -r 3063f6b7a189 -r ac8e534b4834 doc-src/Intro/getting.tex
--- 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.
 
 
diff -r 3063f6b7a189 -r ac8e534b4834 doc-src/Intro/intro.bbl
--- 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.
diff -r 3063f6b7a189 -r ac8e534b4834 doc-src/Intro/intro.tex
--- 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