1.1 --- a/doc-src/HOL/HOL.tex	Mon May 12 14:49:08 2003 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon May 12 15:06:43 2003 +0200
     1.3 @@ -385,14 +385,14 @@
     1.4  \tdx{iffD1}       [| P=Q; P |] ==> Q
     1.5  \tdx{iffD2}       [| P=Q; Q |] ==> P
     1.6  \tdx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
     1.7 +\subcaption{Logical equivalence}
     1.8 +
     1.9 +\end{ttbox}
    1.10 +\caption{Derived rules for HOL} \label{hol-lemmas1}
    1.11 +\end{figure}
    1.12  %
    1.13  %\tdx{eqTrueI}     P ==> P=True 
    1.14  %\tdx{eqTrueE}     P=True ==> P 
    1.15 -\subcaption{Logical equivalence}
    1.16 -
    1.17 -\end{ttbox}
    1.18 -\caption{Derived rules for HOL} \label{hol-lemmas1}
    1.19 -\end{figure}
    1.20  
    1.21  
    1.22  \begin{figure}
    1.23 @@ -846,15 +846,15 @@
    1.24  
    1.25  \tdx{Union_Un_distrib}  Union(A Un B) = (Union A) Un (Union B)
    1.26  \tdx{Int_Union}         A Int (Union B) = (UN C:B. A Int C)
    1.27 -%\tdx{Un_Union_image}    (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
    1.28  
    1.29  \tdx{Inter_Un_distrib}  Inter(A Un B) = (Inter A) Int (Inter B)
    1.30  \tdx{Un_Inter}          A Un (Inter B) = (INT C:B. A Un C)
    1.31 -%\tdx{Int_Inter_image}   (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
    1.32 +
    1.33  \end{ttbox}
    1.34  \caption{Set equalities} \label{hol-equalities}
    1.35  \end{figure}
    1.36 -
    1.37 +%\tdx{Un_Union_image}    (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
    1.38 +%\tdx{Int_Inter_image}   (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
    1.39  
    1.40  Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
    1.41  obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such
    1.42 @@ -1155,10 +1155,10 @@
    1.43          $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
    1.44          & general sum of sets
    1.45  \end{constants}
    1.46 -\begin{ttbox}\makeatletter
    1.47  %\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)
    1.48  %\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)
    1.49  %\tdx{split_def}    split c p == c (fst p) (snd p)
    1.50 +\begin{ttbox}\makeatletter
    1.51  \tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
    1.52  
    1.53  \tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')