--- a/doc-src/Intro/advanced.tex Mon May 02 12:34:56 1994 +0200
+++ b/doc-src/Intro/advanced.tex Tue May 03 10:40:24 1994 +0200
@@ -546,7 +546,7 @@
negate :: "signal => signal"
\end{ttbox}
-\subsection{Infix and Mixfix operators}
+\subsection{Infix and mixfix operators}
\index{infixes}\index{examples!of theories}
Infix or mixfix syntax may be attached to constants. Consider the
@@ -675,8 +675,8 @@
\index{examples!of theories}
\begin{ttbox}
BoolNat = Arith +
-types bool,nat
-arities bool,nat :: arith
+types bool nat
+arities bool, nat :: arith
consts Suc :: "nat=>nat"
\ttbreak
rules add0 "0 + n = n::nat"
--- 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 @@
\begin{itemize}
\item first-order logic, constructive and classical versions
\item higher-order logic, similar to that of Gordon's {\sc
-hol}~\cite{gordon88a}
+hol}~\cite{mgordon-hol}
\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 @@
texts~\cite{galton90,reeves90}.
\index{LCF}
-{\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 @@
\include{advanced}
\bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{string,atp,funprog,general,logicprog,theory}
+\bibliography{string,atp,funprog,general,logicprog,isabelle,theory}
\input{intro.ind}
\end{document}