From d217ba87a3e287612e9bbc99c78682cc9f06133e Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 27 Mar 2015 16:29:09 +0100
Subject: [PATCH] good structure for introduction

---
 doc/intro.rst | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/doc/intro.rst b/doc/intro.rst
index 7f6caa980..fab61d5fe 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
+-----------------
+
-- 
GitLab