doc: small fixes in installation mostly

doc/index.rst

@@ -27,6 +27,5 @@ Indices and tables
 ==================
 
 * :ref:`genindex`
-* :ref:`modindex`
 * :ref:`search`
 

doc/installation.rst

@@ -13,7 +13,7 @@ Windows.
 
 **Requirements:**
 
-* 1.7 Java Development Kit. *(Java 8 is not officially supported)*
+* `1.7  Java Development Kit <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_ *(Java 8 is not officially supported)* 
 
 * SBT 0.13.X (Available from http://www.scala-sbt.org/)
 
@@ -63,7 +63,7 @@ all the appropriate settings:
  
  $ sbt script
 
-You will now need to either port the bash script to Windows, or by running it
+You will now need to either port the bash script to Windows, or to run it
 under Cygwin.
 
 .. _smt-solvers:
@@ -72,20 +72,25 @@ SMT Solvers
 -----------
 
 Leon relies on SMT solvers to solve the constraints it generates. We currently
-support two major SMT solvers: Z3 and CVC4.
+support two major SMT solvers: 
+  * CVC4, http://cvc4.cs.nyu.edu/web/
+  * Z3, https://github.com/Z3Prover/z3
 
 For Linux users, a native Z3 API is bundled with Leon and should work out of the
 box. For OS-X and Windows users, you will either have to recompile the native
 communication layer yourself or use the SMT-LIB API.
 
+Solver binaries that you install should match your operating system and
+your architecture.
+
 In any case, we recommend that you install both solvers separately and have
 their binaries available in the ``$PATH``.
 
 Since the default solver uses the native Z3 API, you will have to explicitly
-specify another solver if this native layer is not available for you:
-
+specify another solver if this native layer is not available for you. Check the
+the ``--solvers`` command line option:
 
-.. code-block:: bash
+:: 
 
  --solvers=s1,s2      Use solvers s1 and s2
                       Available:

doc/r

+make html