diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst
index 2401d2573deca44a23b4b1f0ffa03befd0b15008..09ddf35438b4591f86f21f3446dcee463176685e 100644
--- a/doc/gettingstarted.rst
+++ b/doc/gettingstarted.rst
@@ -94,5 +94,5 @@ and get something like this
 For more details on how to build Leon from sources that can
 be used directly from the shell, see
 :ref:`installation`.  In addition to invoking `./leon --help` you
-may wish to consult :ref:`cmdlineoptions`.
+may wish to consult :ref:`cmdlineoptions` options.
 
diff --git a/doc/library.rst b/doc/library.rst
index b49c3881b89846a88468dcd955b4b4a1f5f97d4d..3778e8e038ee5c81c4780a31ca5be579a2fdfc5c 100644
--- a/doc/library.rst
+++ b/doc/library.rst
@@ -3,7 +3,36 @@
 Leon Library
 ============
 
-Leon defines its own versions of most data structures. One of the reasons is to ensure that these operations can be correctly mapped to mathematical functions and relations inside of SMT solvers, largely defined by the SMT-LIB standard (see http://www.smt-lib.org/).
+Leon defines its own versions of most data structures. One
+of the reasons is to ensure that these operations can be
+correctly mapped to mathematical functions and relations
+inside of SMT solvers, largely defined by the SMT-LIB
+standard (see http://www.smt-lib.org/).
+
+To use Leon's libraries, you need to use the appropriate
+`import` directive at the top of Leon's compilation units.
+Here is a quick summary of what to import.
+
++--------------------------------+----------------------------------------------------+
+| Package to import              | What it gives access to                            |
++================================+====================================================+
+|`leon.annotation`               | Leon annotations, e.g. @induct                     |
++--------------------------------+----------------------------------------------------+
+|`leon.lang`                     | `Map`, `Set`, `holds`, `passes`, `invariant`       |
++--------------------------------+----------------------------------------------------+
+|`leon.collection.List`          | List[T]                                            +
++--------------------------------+----------------------------------------------------+
+|`leon.collection.Option`        | Option[T]                                          +
++--------------------------------+----------------------------------------------------+
+|`leon.lang.string`              | String                                             +
++--------------------------------+----------------------------------------------------+
+|`leon.lang.xlang`               | epsilon                                            +
++--------------------------------+----------------------------------------------------+
+|`leon.lang.synthesis`           | choose, ???, ?, ?!                                 +
++--------------------------------+----------------------------------------------------+
+
+In the sequel we outline some of the libraries. To learn more, we encourage you to
+look in the `library/` subdirectory of Leon distribution.
 
 List
 ^^^^