summaryrefslogtreecommitdiff
path: root/theories/Relations/intro.tex
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Relations/intro.tex')
-rwxr-xr-xtheories/Relations/intro.tex23
1 files changed, 0 insertions, 23 deletions
diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex
deleted file mode 100755
index 5056f36f..00000000
--- a/theories/Relations/intro.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\section{Relations}\label{Relations}
-
-This library develops closure properties of relations.
-
-\begin{itemize}
-\item {\tt Relation\_Definitions.v} deals with the general notions
- about binary relations (orders, equivalences, ...)
-
-\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
- closures of relations (by symmetry, by transitivity, ...) and
- lexicographic orderings.
-
-\item {\tt Operators\_Properties.v} states and proves facts on the
- various closures of a relation.
-
-\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
- Relation\_Operators.v} and \\
- {\tt Operators\_Properties.v} together.
-
-\item {\tt Newman.v} proves Newman's lemma on noetherian and locally
- confluent relations.
-
-\end{itemize}