1.1 --- a/doc-src/Logics/Old_HOL.tex	Thu Nov 11 13:24:47 1993 +0100
     1.2 +++ b/doc-src/Logics/Old_HOL.tex	Fri Nov 12 10:41:13 1993 +0100
     1.3 @@ -525,7 +525,7 @@
     1.4  \idx{Collect_mem_eq}    \{x.x:A\} = A
     1.5  \subcaption{Isomorphisms between predicates and sets}
     1.6  
     1.7 -\idx{empty_def}         \{\}         == \{x.x= False\}
     1.8 +\idx{empty_def}         \{\}          == \{x.x= False\}
     1.9  \idx{insert_def}        insert(a,B) == \{x.x=a\} Un B
    1.10  \idx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
    1.11  \idx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
    1.12 @@ -599,7 +599,7 @@
    1.13  
    1.14  \idx{insertI1} a : insert(a,B)
    1.15  \idx{insertI2} a : B ==> a : insert(b,B)
    1.16 -\idx{insertE}  [| a : insert(b,A);  a=b ==> P;  a:A ==> P |] ==> 
    1.17 +\idx{insertE}  [| a : insert(b,A);  a=b ==> P;  a:A ==> P |] ==> P
    1.18  
    1.19  \idx{ComplI}   [| c:A ==> False |] ==> c : Compl(A)
    1.20  \idx{ComplD}   [| c : Compl(A) |] ==> ~ c:A
    1.21 @@ -1144,7 +1144,7 @@
    1.22  \section{The examples directories}
    1.23  Directory {\tt Subst} contains Martin Coen's mechanization of a theory of
    1.24  substitutions and unifiers.  It is based on Paulson's previous
    1.25 -mechanization in {\LCF}~\cite{paulson85} of theory Manna and Waldinger's
    1.26 +mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's
    1.27  theory~\cite{mw81}. 
    1.28  
    1.29  Directory {\tt ex} contains other examples and experimental proofs in
    1.30 @@ -1268,8 +1268,8 @@
    1.31  By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of
    1.32  the vacuous one and put the other into a convenient form:\footnote
    1.33  {In higher-order logic, {\tt spec RS mp} fails because the resolution yields
    1.34 -two results, namely $\List{\forall x.x; P}\Imp Q$ and $\List{\forall
    1.35 -  x.P(x)\imp Q(x); P(x)}\Imp Q(x)$.  In first-order logic, the resolution
    1.36 +two results, namely ${\List{\forall x.x; P}\Imp Q}$ and ${\List{\forall
    1.37 +  x.P(x)\imp Q(x); P(x)}\Imp Q(x)}$.  In first-order logic, the resolution
    1.38  yields only the latter result.}
    1.39  \index{*RL}
    1.40  \begin{ttbox}