# HG changeset patch
# User lcp
# Date 767954424 7200
# Node ID 1f5a94209c972c176a14d6a22d3d3eb15ac0270e
# Parent cd41a57221d07441647284e239b8d8d77d498ef5
postCRC corrections
diff r cd41a57221d0 r 1f5a94209c97 docsrc/Intro/advanced.tex
 a/docsrc/Intro/advanced.tex Mon May 02 12:34:56 1994 +0200
+++ b/docsrc/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"
diff r cd41a57221d0 r 1f5a94209c97 docsrc/Intro/intro.tex
 a/docsrc/Intro/intro.tex Mon May 02 12:34:56 1994 +0200
+++ b/docsrc/Intro/intro.tex Tue May 03 10:40:24 1994 +0200
@@ 43,7 +43,7 @@
\begin{itemize}
\item firstorder logic, constructive and classical versions
\item higherorder logic, similar to that of Gordon's {\sc
hol}~\cite{gordon88a}
+hol}~\cite{mgordonhol}
\item ZermeloFraenkel set theory~\cite{suppes72}
\item an extensional version of MartinL\"of's Type Theory~\cite{nordstrom90}
\item the classical firstorder 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,paulsonhandbook}
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, objectlogics 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 higherorder metalogic 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}