\section{Sets}\label{Sets}

This is a library on sets defined by their characteristic predicate.
It contains the following modules:

\begin{itemize}
\item {\tt Ensembles.v}
\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v}
\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, 
 {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v},  \\
 {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v}
\item {\tt Partial\_Order.v}, {\tt Cpo.v}
\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, 
 {\tt Powerset\_Classical\_facts.v}
\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v}
\item {\tt Image.v}
\item {\tt Infinite\_sets.v}
\item {\tt Integers.v}
\end{itemize}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: