doc: what to import.

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.
 

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
 ^^^^