changeset 348 1f5a94209c97
parent 311 3fb8cdb32e10
child 873 0cfc734e3dbd
--- a/doc-src/Intro/intro.tex	Mon May 02 12:34:56 1994 +0200
+++ b/doc-src/Intro/intro.tex	Tue May 03 10:40:24 1994 +0200
@@ -43,7 +43,7 @@
 \item first-order logic, constructive and classical versions
 \item higher-order logic, similar to that of Gordon's {\sc
 \item Zermelo-Fraenkel set theory~\cite{suppes72}
 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
 \item the classical first-order sequent calculus, {\sc lk}
@@ -68,7 +68,7 @@
-{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an
+{\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
 ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
 abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
@@ -76,15 +76,6 @@
 by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
 helpful in understanding the relationship between {\sc lcf} and Isabelle.
-Isabelle does not keep a record of inference steps.  Each step is checked
-at run time to ensure that theorems can only be constructed by applying
-inference rules.  An Isabelle proof typically involves hundreds of
-primitive inferences, and would be unintelligible if displayed.
-Discarding proofs saves vast amounts of storage.  But can Isabelle be
-trusted?  If desired, object-logics can be formalized such that each
-theorem carries a proof term, which could be checked by another program.
-Proofs can also be traced.
 \index{Isabelle!release history} Isabelle was first distributed in 1986.
 The 1987 version introduced a higher-order meta-logic with an improved
 treatment of quantifiers.  The 1988 version added limited polymorphism and
@@ -142,7 +133,7 @@
 \bibliographystyle{plain} \small\raggedright\frenchspacing