1 files changed, 0 insertions, 24 deletions
diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex
deleted file mode 100755
index 83c2177f..00000000
--- a/theories/Sets/intro.tex
+++ /dev/null
@@ -1,24 +0,0 @@
-\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: