diff --git a/build.sbt b/build.sbt
index fae3a337f666e4b53f65e60e66171d59aea1fff2..de14da5952368a72ed5f88fd42c10af7599f5b63 100644
--- a/build.sbt
+++ b/build.sbt
@@ -12,6 +12,8 @@ scalacOptions ++= Seq(
   "-feature"
 )
 
+scalacOptions in (Compile, doc) ++= Seq("-doc-root-content", baseDirectory.value+"/src/main/scala/root-doc.txt")
+
 javacOptions += "-Xlint:unchecked"
 
 if(System.getProperty("sun.arch.data.model") == "64") {
diff --git a/src/main/scala/leon/package.scala b/src/main/scala/leon/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..92e4b7a03b4b7784807218585106a63d95eab368
--- /dev/null
+++ b/src/main/scala/leon/package.scala
@@ -0,0 +1,5 @@
+/** Core package of the Leon system 
+  *
+  * Provides the basic types and definitions for the Leon system.
+  */
+package object leon { }
diff --git a/src/main/scala/root-doc.txt b/src/main/scala/root-doc.txt
new file mode 100644
index 0000000000000000000000000000000000000000..9f01546cc61ad0c4122a05b89fe16d4cdc3e95e4
--- /dev/null
+++ b/src/main/scala/root-doc.txt
@@ -0,0 +1,37 @@
+This is the documentation for the Leon system
+
+==Structure==
+
+Leon is organized similarly to a compiler with a concept of [[leon.Pipeline]]
+and [[leon.LeonPhase]]. The main phases of Leon are implemented in subpackages, with
+an overview of the role of each of them below.
+
+The definition of the Pure Scala AST is in [[leon.purescala]]. Most of the other packages
+are articulated around the definitions of these ASTs. The [[leon.xlang]] provides extensions
+to the Pure Scala AST, but most of the other packages will ignore these extensions and
+assume a Pure Scala only AST.
+
+  - [[leon.codegen]] provides bytecode generator for Leon programs. Enable the conversion of a [[leon.purescala.Definitions.Program]] to JVM bytecode.
+
+  - [[leon.datagen]] provides a generator of expressions (trees), based on vanuatoo.
+
+  - [[leon.evaluators]] implements different evaluators for Leon programs in Pure Scala. 
+
+  - [[leon.frontends]] provides the different front-ends to Leon. Currently it only implements a scalac integration, but it could potentially support other language.
+
+  - [[leon.purescala]] defines the core AST for Pure Scala. Also provides useful tree manipulation methods.
+
+  - [[leon.repair]] implements the Repair module of Leon.
+
+  - [[leon.solvers]] provides an interface and implementations to solvers for Pure Scala expressions. The solvers are typically wrappers around SMT solvers, with some additional algorithms to handle recursive function invocations.
+
+  - [[leon.synthesis]] implements the Synthesis module of Leon.
+
+  - [[leon.termination]] implements the termination checker of Leon.
+
+  - [[leon.utils]]
+
+  - [[leon.verification]] implements the verification module of Leon.
+
+  - [[leon.xlang]] provides extensions to Pure Scala. In particular, it introduces some expressions to represent imperative programs. Also provides the code to map such programs to Pure Scala equivalent ones.
+