diff --git a/README b/README
new file mode 100644
index 0000000000000000000000000000000000000000..6604deb78b9fd27b8890a3a57dd701c92208c189
--- /dev/null
+++ b/README
@@ -0,0 +1,45 @@
+This is Leon 0.2.0
+
+To build it, you will need, for example, the following:
+  * Java Runtime Environment, from Oracle, e.g. Version 7 Update 5 
+    (to run xsbt and scala)
+  * Scala, from Typesafe, e.g. version 2.9.1
+  * xsbt, e.g. version 0.11.3: download sbt-launch.jar, run it with java -jar
+    (to built Leon)
+  * a recent GLIBC3 or later, works with e.g. apt-get
+    (for Z3)
+  * GNU Multiprecision library, e.g. gmp3, works with e.g. apt-get
+    (for Z3)
+
+To build, type this:
+
+xsbt clean   
+xsbt package # takes a while
+xsbt script
+
+Then you can try e.g.
+
+./run-demo demo/RedBlackTree.scala
+
+and get something like this:
+
+[ Info  ] . ┌─────────┐
+          ╔═╡ Summary ╞═══════════════════════════════════════════════════════════════════════╗
+          ║ └─────────┘                                                                       ║
+          â•‘ add                       postcond.           valid               Z3-f+t    0.314 â•‘
+          â•‘ add                       precond.    (82,14) valid               Z3-f+t    0.020 â•‘
+          â•‘ add                       precond.    (82,18) valid               Z3-f+t    0.005 â•‘
+          â•‘ balance                   postcond.           valid               Z3-f+t    0.409 â•‘
+          â•‘ balance                   match.      (91,19) valid               Z3-f+t    0.034 â•‘
+          â•‘ blackHeight               match.      (51,39) valid               Z3-f+t    0.004 â•‘
+          â•‘ buggyAdd                  postcond.           invalid             Z3-f+t    4.084 â•‘
+          â•‘ buggyAdd                  precond.     (87,8) invalid             Z3-f+t    0.111 â•‘
+          â•‘ buggyBalance              postcond.           invalid             Z3-f+t    0.055 â•‘
+          â•‘ buggyBalance              match.     (105,19) invalid             Z3-f+t    0.007 â•‘
+          â•‘ ins                       postcond.           valid               Z3-f+t    6.577 â•‘
+          â•‘ ins                       precond.    (63,40) valid               Z3-f+t    0.021 â•‘
+          â•‘ ins                       precond.    (65,43) valid               Z3-f+t    0.005 â•‘
+          â•‘ makeBlack                 postcond.           valid               Z3-f+t    0.007 â•‘
+          â•‘ redNodesHaveBlackChildren match.      (35,56) valid               Z3-f+t    0.003 â•‘
+          â•‘ size                      postcond.           valid               Z3-f+t    0.012 â•‘
+          ╚═══════════════════════════════════════════════════════════════════════════════════╝