author wenzelm Thu Nov 25 15:32:42 1993 +0100 (1993-11-25) changeset 154 f8c3715457b8 parent 153 0deb993885ce child 155 f58571828c68
corrected obvious errors;
     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)