diff --git a/doc/options.rst b/doc/options.rst
index b4462aa13d1809a34a48f517890e0a0319c1144e..82f52a7ff8c100b17dccec7a93cb4cd16cf31b25 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -1,7 +1,7 @@
 .. _cmdlineoptions:
 
-Command Line Options
-====================
+Command Line
+============
 
 Here is an overview of the command-line options that Leon recognizes: 
 
diff --git a/doc/purescala.rst b/doc/purescala.rst
index b8236f09e459598e5a7a410d18291dc1a5eb342d..7c9f7e6ceb4f00f53ced5448f3618bca36e2a65d 100644
--- a/doc/purescala.rst
+++ b/doc/purescala.rst
@@ -3,12 +3,13 @@
 Pure Scala
 ==========
 
-The input to Leon is a purely functional subset of Scala,
-which we call **Pure Scala**. Constructs specific for Leon
-are defined inside Leon's libraries in package `leon` and
-its subpackages. Leon invokes standard `scalac` compiler on
-the input file, then performs additional checks to ensure
-that the given program belongs to Pure Scala.
+The input to Leon is a purely functional **subset** of Scala
+(http://www.scala-lang.org/), which we call 
+**Pure Scala**. Constructs specific for Leon are defined inside
+Leon's libraries in package `leon` and its subpackages. Leon
+invokes standard `scalac` compiler on the input file, then
+performs additional checks to ensure that the given program
+belongs to Pure Scala.
 
 Pure Scala supports two kinds of top-level declarations:
 
diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index f4dce6b9541320b72e0f7ffecc776151a6d53454..0e83c638a9cff20be1e9b7dea8ad4e273569f080 100644
--- a/doc/tutorial.rst
+++ b/doc/tutorial.rst
@@ -92,8 +92,8 @@ parameters, such as
 
     def test1 = sort2(30, 4)
 
-Hovering over the definition of test1 should display
-the computed tuple `(4,30)`.
+Hovering over `test1` should display the computed result
+`(4,30)`. From :ref:`cmdlineoptions`, use `--eval`.
 
 This shows that Leon's evaluator can also execute `choose`
 constructs. In other words, it supports programming
@@ -136,16 +136,23 @@ Depending on the particular run, Leon may also produce a solution such as
 
 This code performs some unnecessary case analysis, but still
 satisfies our specification. In this case, the specification
-is unambiguous, so all programs that one can synthesize
-compute the same results for all inputs.
+of the program output is unambiguous, so all programs that
+one can synthesize compute the same results for all inputs.
 
-Defining Unbounded Lists
-------------------------
+Defining Lists and Their Properties
+-----------------------------------
 
-Let us now consider sorting of any number of elements.
+We next consider sorting an unbounded number of elements.
 
-For this purpose, we define the data structure of lists of
-(big) integers.  Leon has a built-in data type of
-polymorphic lists, see :ref:`Leon Library <library>`, but
-here we define our own variant.
+For this purpose, we define a data structure for lists of
+integers.  Leon has a built-in data type of parametric
+lists, see :ref:`Leon Library <library>`, but here we define
+our own variant instead. We use a recursive algebraic data type
+definition, expressed using Scala's **case classes**.
+
+.. code-block:: scala
+
+  sealed abstract class List
+  case object Nil extends List
+  case class Cons(head: BigInt, tail: List) extends List