summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 22 Jul 1996 16:16:51 +0200 | |

changeset 1878 | ac8e534b4834 |

parent 1877 | 3063f6b7a189 |

child 1879 | 83c70ad381c1 |

Updated BibTeX identifiers

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