doc-src/Intro/foundations.tex
 changeset 1878 ac8e534b4834 parent 1865 484956c42436 child 3103 98af809fee46
--- 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