diff --git a/doc/index.rst b/doc/index.rst
index 2862cb2a406384e7a7797c8fff673b03192ec633..34b763386b3611235047d47656fa82b7ec1cba54 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -16,6 +16,7 @@ Contents:
    tutorial
    installation
    purescala
+   library
    xlang
    verification
    synthesis
diff --git a/doc/library.rst b/doc/library.rst
new file mode 100644
index 0000000000000000000000000000000000000000..b49c3881b89846a88468dcd955b4b4a1f5f97d4d
--- /dev/null
+++ b/doc/library.rst
@@ -0,0 +1,20 @@
+.. _library:
+
+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/).
+
+List
+^^^^
+
+Set
+^^^
+
+Option
+^^^^^^
+
+Map
+^^^
+
+
diff --git a/doc/purescala.rst b/doc/purescala.rst
index 2402c730f156533fb3d2099c65502ee67c5e7094..3c10fd4bf4f2e02a61c2aa00143e6039eb185b96 100644
--- a/doc/purescala.rst
+++ b/doc/purescala.rst
@@ -1,7 +1,7 @@
 .. _purescala:
 
-Pure Scala
-=============================
+Pure Scala: Leon's Core Input Language
+======================================
 
 
 Leon supports two kinds of top-level declarations:
diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index 8a84a5db58d0fe12a5af11b90f67374e599b9276..90ff3d572653b8cf39673c51330c1284d8156c5f 100644
--- a/doc/tutorial.rst
+++ b/doc/tutorial.rst
@@ -1,7 +1,31 @@
 .. _tutorial:
 
-Tutorial
-========
+Tutorials
+=========
+
+Sorting Lists
+-------------
+
+This tutorial shows how to define lists as algebraic data
+types, how to **verify** certain properties of an insertion
+sort, as well as how to use Leon to **synthesize**
+operations from specifications.
+
+Defining lists
+^^^^^^^^^^^^^^
+
+Leon has a built-in data type of polymorphic lists (see 
+
+Let us start by specifying a function that sorts **two**
+mathematical integers.
+
+.. code-block:: scala
+
+  import leon.lang._
+  import leon.lang.synthesis._
+  object Sort {
+    def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) =>
+      Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
+    }
+  }
 
-In this section, we will go through an extended tutorial to demonstrate basic
-usage of Leon.