From 4ac0580306ea9e45da1863316936d700969465ad Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 11 Apr 2001 12:41:41 +0000
Subject: documentation automatique de la bibliothèque standard
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Sets/intro.tex | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100755 theories/Sets/intro.tex

(limited to 'theories/Sets/intro.tex')

diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex
new file mode 100755
index 000000000..83c2177fd
--- /dev/null
+++ b/theories/Sets/intro.tex
@@ -0,0 +1,24 @@
+\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: 
-- 
cgit v1.2.3