1.1 --- a/doc-src/Intro/advanced.tex	Mon May 02 12:34:56 1994 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Tue May 03 10:40:24 1994 +0200
     1.3 @@ -546,7 +546,7 @@
     1.4         negate :: "signal => signal"
     1.5  \end{ttbox}
     1.6  
     1.7 -\subsection{Infix and Mixfix operators}
     1.8 +\subsection{Infix and mixfix operators}
     1.9  \index{infixes}\index{examples!of theories}
    1.10  
    1.11  Infix or mixfix syntax may be attached to constants.  Consider the
    1.12 @@ -675,8 +675,8 @@
    1.13  \index{examples!of theories}
    1.14  \begin{ttbox}
    1.15  BoolNat = Arith +
    1.16 -types   bool,nat
    1.17 -arities bool,nat    :: arith
    1.18 +types   bool  nat
    1.19 +arities bool, nat   :: arith
    1.20  consts  Suc         :: "nat=>nat"
    1.21  \ttbreak
    1.22  rules   add0        "0 + n = n::nat"

     2.1 --- a/doc-src/Intro/intro.tex	Mon May 02 12:34:56 1994 +0200
     2.2 +++ b/doc-src/Intro/intro.tex	Tue May 03 10:40:24 1994 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4  \begin{itemize}
     2.5  \item first-order logic, constructive and classical versions
     2.6  \item higher-order logic, similar to that of Gordon's {\sc
     2.7 -hol}~\cite{gordon88a}
     2.8 +hol}~\cite{mgordon-hol}
     2.9  \item Zermelo-Fraenkel set theory~\cite{suppes72}
    2.10  \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
    2.11  \item the classical first-order sequent calculus, {\sc lk}
    2.12 @@ -68,7 +68,7 @@
    2.13  texts~\cite{galton90,reeves90}.
    2.14  
    2.15  \index{LCF}
    2.16 -{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an
    2.17 +{\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
    2.18  ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
    2.19  ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
    2.20  abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
    2.21 @@ -76,15 +76,6 @@
    2.22  by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
    2.23  helpful in understanding the relationship between {\sc lcf} and Isabelle.
    2.24  
    2.25 -Isabelle does not keep a record of inference steps.  Each step is checked
    2.26 -at run time to ensure that theorems can only be constructed by applying
    2.27 -inference rules.  An Isabelle proof typically involves hundreds of
    2.28 -primitive inferences, and would be unintelligible if displayed.
    2.29 -Discarding proofs saves vast amounts of storage.  But can Isabelle be
    2.30 -trusted?  If desired, object-logics can be formalized such that each
    2.31 -theorem carries a proof term, which could be checked by another program.
    2.32 -Proofs can also be traced.
    2.33 -
    2.34  \index{Isabelle!release history} Isabelle was first distributed in 1986.
    2.35  The 1987 version introduced a higher-order meta-logic with an improved
    2.36  treatment of quantifiers.  The 1988 version added limited polymorphism and
    2.37 @@ -142,7 +133,7 @@
    2.38  \include{advanced}
    2.39  
    2.40  \bibliographystyle{plain} \small\raggedright\frenchspacing
    2.41 -\bibliography{string,atp,funprog,general,logicprog,theory}
    2.42 +\bibliography{string,atp,funprog,general,logicprog,isabelle,theory}
    2.43  
    2.44  \input{intro.ind}
    2.45  \end{document}