1 files changed, 62 insertions, 0 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
new file mode 100755
index 00000000..97748af6
--- /dev/null
+++ b/doc/stdlib/Library.tex
@@ -0,0 +1,62 @@
+\documentclass[11pt]{article}
+
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+
+\input{../common/version}
+\input{../common/title}
+\input{../common/macros}
+
+\begin{document}
+ 
+\coverpage{The standard library}%
+{\ }
+{This material is distributed under the terms of the GNU Lesser
+General Public License Version 2.1.}
+
+\tableofcontents
+
+\newpage
+\section*{The \Coq\ standard library}
+
+This document is a short description of the \Coq\ standard library.
+This library comes with the system as a complement of the core library
+(the {\bf Init} library ; see the Reference Manual for a description
+of this library). It provides a set of modules directly available
+through the \verb!Require! command.
+
+The standard library is composed of the following subdirectories:
+\begin{description}
+  \item[Logic]  Classical logic and dependent equality
+  \item[Bool]   Booleans (basic functions and results)
+  \item[Arith]  Basic Peano arithmetic
+  \item[ZArith] Basic integer arithmetic
+  \item[Reals]  Classical Real Numbers and Analysis
+  \item[Lists]  Monomorphic and polymorphic lists (basic functions and
+                  results), Streams (infinite sequences defined 
+                  with co-inductive types)
+  \item[Sets]   Sets (classical, constructive, finite, infinite, power set,
+                  etc.)
+  \item[Relations] Relations (definitions and basic results).
+  \item[Sorting] Sorted list (basic definitions and heapsort
+                 correctness). 
+  \item[Wellfounded] Well-founded relations (basic results).
+  \item[IntMap]       Representation of finite sets by an efficient
+                     structure of map (trees indexed by binary integers).
+\end{description}
+
+
+Each of these subdirectories contains a set of modules, whose
+specifications (\gallina{} files) have
+been roughly, and automatically, pasted in the following pages. There
+is also a version of this document in HTML format on the WWW, which
+you can access from the \Coq\ home page at
+\texttt{http://coq.inria.fr/library}.
+
+\input{Library.coqdoc}
+
+\end{document}
+
+% $Id: Library.tex 8626 2006-03-14 15:01:00Z notin $