corrected obvious errors;
authorwenzelm
Thu Nov 25 15:32:42 1993 +0100 (1993-11-25)
changeset 154f8c3715457b8
parent 153 0deb993885ce
child 155 f58571828c68
corrected obvious errors;
doc-src/Logics/Old_HOL.tex
     1.1 --- a/doc-src/Logics/Old_HOL.tex	Thu Nov 25 15:15:53 1993 +0100
     1.2 +++ b/doc-src/Logics/Old_HOL.tex	Thu Nov 25 15:32:42 1993 +0100
     1.3 @@ -471,7 +471,7 @@
     1.4  \begin{tabular}{rrr} 
     1.5    \it external          & \it internal  & \it description \\ 
     1.6    $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm negated membership\\
     1.7 -  \{$a@1$, $\ldots$, $a@n$\}  &  insert($a@1$,$\cdots$,insert($a@n$,0)) &
     1.8 +  \{$a@1$, $\ldots$, $a@n$\}  &  insert($a@1$,$\cdots$,insert($a@n$,\{\})) &
     1.9          \rm finite set \\
    1.10    \{$x$.$P[x]$\}        &  Collect($\lambda x.P[x]$) &
    1.11          \rm comprehension \\
    1.12 @@ -525,7 +525,7 @@
    1.13  \idx{Collect_mem_eq}    \{x.x:A\} = A
    1.14  \subcaption{Isomorphisms between predicates and sets}
    1.15  
    1.16 -\idx{empty_def}         \{\}          == \{x.x= False\}
    1.17 +\idx{empty_def}         \{\}          == \{x.x=False\}
    1.18  \idx{insert_def}        insert(a,B) == \{x.x=a\} Un B
    1.19  \idx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
    1.20  \idx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
    1.21 @@ -670,7 +670,7 @@
    1.22  sets constructed in the obvious manner using~{\tt insert} and~$\{\}$ (the
    1.23  empty set):
    1.24  \begin{eqnarray*}
    1.25 - \{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\emptyset)))
    1.26 + \{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\{\})))
    1.27  \end{eqnarray*}
    1.28  
    1.29  The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)