diff --git a/doc/intro.rst b/doc/intro.rst
index 7f6caa98033fbb4fdffa1174519a1c82e68dee9c..fab61d5fec10a2eda50a7f051936a3bcd4f2831c 100644
--- a/doc/intro.rst
+++ b/doc/intro.rst
@@ -46,4 +46,20 @@ following:
   postcondition does not hold. Leon will always return a concrete counterexample, very
   useful when trying to understand why a function is not satisfying its contract.
 * The postcondition is `unknown`. It means Leon is unable to prove or find a counterexample.
-  It usually happens after a timeout or an internal error in the external theorem prover. 
+  It usually happens after a timeout or an internal error occuring in the external 
+  theorem prover. 
+
+Leon will also verify for each call site that the precondition of the invoked
+function cannot be violated.
+
+Leon supports verification of a significant part of the Scala language, described in the
+sections :ref:`Pure Scala <purescala>` and :ref:`XLang <xlang>`.
+
+
+Automated Repair of Programs
+----------------------------
+
+
+Program Synthesis
+-----------------
+