doc-src/Logics/Old_HOL.tex
 changeset 841 14b96e3bd4ab parent 705 9fb068497df4 child 861 28a593f4b600
equal inserted replaced
840:5716e174b591 841:14b96e3bd4ab
   602 \begin{figure} \underscoreon
   602 \begin{figure} \underscoreon
   603 \begin{ttbox}
   603 \begin{ttbox}
   604 \tdx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
   604 \tdx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
   605 \tdx{Collect_mem_eq}    \{x.x:A\} = A
   605 \tdx{Collect_mem_eq}    \{x.x:A\} = A
   606
   606
   607 \tdx{empty_def}         \{\}          == \{x.x=False\}
   607 \tdx{empty_def}         \{\}          == \{x.False\}
   608 \tdx{insert_def}        insert(a,B) == \{x.x=a\} Un B
   608 \tdx{insert_def}        insert(a,B) == \{x.x=a\} Un B
   609 \tdx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
   609 \tdx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
   610 \tdx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
   610 \tdx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
   611 \tdx{subset_def}        A <= B      == ! x:A. x:B
   611 \tdx{subset_def}        A <= B      == ! x:A. x:B
   612 \tdx{Un_def}            A Un B      == \{x.x:A | x:B\}
   612 \tdx{Un_def}            A Un B      == \{x.x:A | x:B\}