doc: remove some redundancy, add crossrefs

doc/gettingstarted.rst

@@ -93,7 +93,8 @@ 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`. 
+:ref:`installation`.  In addition to invoking `./leon --help` you
+may wish to consult :ref:`cmdlineoptions`.
 
 
 Asking Questions

doc/installation.rst

@@ -88,20 +88,5 @@ 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 to you. Check the
-the ``--solvers`` command line option:
-
-:: 
-
- --solvers=s1,s2      Use solvers s1 and s2
-                      Available:
-                        enum           : Enumeration-based counter-example-finder
-                        fairz3         : Native Z3 with z3-templates for unfolding (default)
-                        smt-cvc4       : CVC4 through SMT-LIB
-                        smt-cvc4-cex   : CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only
-                        smt-cvc4-proof : CVC4 through SMT-LIB, in-solver inductive reasonning, for proofs only
-                        smt-z3         : Z3 through SMT-LIB
-                        smt-z3-q       : Z3 through SMT-LIB, with quantified encoding
-                        unrollz3       : Native Z3 with leon-templates for unfolding
-
-
+specify another solver if this native layer is not available to you. Check also the
+the ``--solvers`` in :ref:`cmdlineoptions` .

doc/options.rst

+.. _cmdlineoptions:
+
 Command Line Options
 ====================
 
 Here is an overview of the command-line options that Leon recognizes: 
 
-Choosing the feature to use:
-----------------------------
+Choosing the feature to use
+---------------------------
 
 The first group of options determine which feature of Leon will be used. They are mutually exclusive,
 with ``--verify`` being the default.

doc/purescala.rst

 .. _purescala:
 
-Pure Scala: Leon's Language
-===========================
+Pure Scala
+==========
 
 The input to Leon is a purely functional subset of Scala,
 which we call **Pure Scala**. Constructs specific for Leon

doc/tutorial.rst

 .. _tutorial:
 
-Tutorials
-=========
+Tutorial: Sorting
+=================
 
-For these tutorials we occasionally assume that the user is using the web 
-interface. The functionality is also available (possibly with less
-convenient interface) from the command line, see :ref:`gettingstarted`.
+This tutorial shows how to:
 
-Sorting Lists
--------------
+  * define lists as algebraic data types
+  * specify sortedness of a list and use function contracts
+  * verify properties of an insertion into a sorted list
+  * execute or synthesize provably correct operations using specifications alone,
+    without the need to write implementation
 
-This tutorial shows how to define lists as algebraic data
-types, how to **verify** certain properties of an insertion
-sort. We finish showing how to use Leon to **synthesize**
-provably correct operations from specifications.
+For this tutorial we occasionally assume that the user is using the web 
+interface. The functionality is also available (possibly with less
+convenient interface) from the command line, see :ref:`gettingstarted`.
 
-A Preview of Specification and Synthesis
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Sorting Two Elements
+--------------------
 
 As a preview, let us start by **specifying** a function that
 sorts **two** mathematical integers. Here is what we need
@@ -82,7 +82,7 @@ length two.  Note that the result is uniquely specified, no
 matter what the values of `x` and `y` are.
 
 Evaluating exppressions containing choose
-.........................................
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Leon contains a built-in evaluator. To see it in action in
 the web interface, just define a function without
@@ -105,7 +105,7 @@ more efficient code. Leon can automate this process
 in some cases, using **synthesis**.
 
 Synthesizing the sort of two elements
-.....................................
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Instead of executing `choose` using a constraint solver
 during execution, we can alternatively instruct Leon to
@@ -139,13 +139,13 @@ satisfies our specification. In this case, the specification
 is unambiguous, so all programs that one can synthesize
 compute the same results for all inputs.
 
-Defining lists
-^^^^^^^^^^^^^^
+Defining Unbounded Lists
+------------------------
 
 Let us now consider sorting of any number of elements.
 
 For this purpose, we define the data structure of lists of
-(big) integers.  (Leon has a built-in data type of
+(big) integers.  Leon has a built-in data type of
 polymorphic lists, see :ref:`Leon Library <library>`, but
-here we will define our own variant.)
+here we define our own variant.