From 9c94091861b7c12ec8c8b3242146c7150517952c Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 24 Apr 2015 20:46:53 +0200
Subject: [PATCH] starting to discuss leon as a theorem prover

---
 doc/verification.rst | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/doc/verification.rst b/doc/verification.rst
index 383292b39..e19b1168f 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -218,3 +218,12 @@ relying on the given precondition.
 
 Proving mathematical theorems with Leon
 ---------------------------------------
+
+As we have seen, verifying the contract of a function is really proving a mathematical
+theorem. In some sense, Leon can be seen as a (mostly) automated theorem prover. It is
+automated in the sense that once the property stated, Leon will proceed with searching
+for a proof without any user interaction. In practice however, many theorems will be fairly
+difficult to prove, and it is possible for the user to provide hints to Leon. 
+  
+Hints typically take the form of simpler properties that combine in order to prove
+more complicated ones.
-- 
GitLab