diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 12:41:41 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 12:41:41 +0000 |
commit | 4ac0580306ea9e45da1863316936d700969465ad (patch) | |
tree | bf7595cd76895f3a349e7e75ca9d64231b01dcf8 /theories/Relations | |
parent | 8a7452976731275212f0c464385b380e2d590f5e (diff) |
documentation automatique de la bibliothèque standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Relations')
-rwxr-xr-x | theories/Relations/intro.tex | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex new file mode 100755 index 000000000..5056f36f9 --- /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} |