1 files changed, 23 insertions, 0 deletions
diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex
new file mode 100755
index 00000000..5056f36f
--- /dev/null
+++ b/theories/Relations/intro.tex
@@ -0,0 +1,23 @@
+\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}