diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst
new file mode 100644
index 0000000000000000000000000000000000000000..3ce1d78a117c4c8b1b614c6109375044d1f88568
--- /dev/null
+++ b/doc/gettingstarted.rst
@@ -0,0 +1,2 @@
+Getting Started
+===============
diff --git a/doc/index.rst b/doc/index.rst
index 38b182c638f9679aa0aff79e2872d588b7a23864..9ffe65702d89d8cf1ad5cce2c3d7ecc396de9887 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -12,7 +12,12 @@ Contents:
    :maxdepth: 2
 
    intro
+   installation
+   gettingstarted
    purescala
+   verification
+   synthesis
+   repair
    references
 
 
diff --git a/doc/installation.rst b/doc/installation.rst
new file mode 100644
index 0000000000000000000000000000000000000000..a013779e78ddccb6687e4a9b4d275f913252e6a1
--- /dev/null
+++ b/doc/installation.rst
@@ -0,0 +1,13 @@
+Installing Leon
+===============
+
+
+
+Linux
+-----
+
+Mac OS-X
+--------
+
+Windows
+-------
diff --git a/doc/intro.rst b/doc/intro.rst
index 3c87dc90d2b20477263d5e9cd3cc53d5365061cd..389973660bc967b7536bde6bec8cec918e48dbc3 100644
--- a/doc/intro.rst
+++ b/doc/intro.rst
@@ -6,14 +6,3 @@ The Leon system is an automated system for verifying, repairing, and synthesizin
 Leon supports programs written in :ref:`purescala`, a purely functional subset of Scala.
 
 
-Verification
-------------
-
-Repair
-------------
-
-Synthesis
-------------
-
-Termination
-------------
diff --git a/doc/repair.rst b/doc/repair.rst
new file mode 100644
index 0000000000000000000000000000000000000000..1a881b7ed6ab7f73fc59073b4c7528371fd9e3ce
--- /dev/null
+++ b/doc/repair.rst
@@ -0,0 +1,2 @@
+Repair
+======
diff --git a/doc/synthesis.rst b/doc/synthesis.rst
new file mode 100644
index 0000000000000000000000000000000000000000..8b283bcd2d42147677503a7a4d07513e1f50749f
--- /dev/null
+++ b/doc/synthesis.rst
@@ -0,0 +1,2 @@
+Synthesis
+=========
diff --git a/doc/verification.rst b/doc/verification.rst
new file mode 100644
index 0000000000000000000000000000000000000000..0e63a08684234d3e5360656c415bcc87825d045d
--- /dev/null
+++ b/doc/verification.rst
@@ -0,0 +1,2 @@
+Verification
+============