diff --git a/build.sbt b/build.sbt
index b6f869108558f3886e7df443329f053a0569a631..feada3374002c48ce63ee6c491869ba12317e9fa 100644
--- a/build.sbt
+++ b/build.sbt
@@ -31,7 +31,7 @@ resolvers ++= Seq(
   "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
 )
 
-val libisabelleVersion = "0.1.2"
+val libisabelleVersion = "0.2"
 
 libraryDependencies ++= Seq(
   "org.scala-lang" % "scala-compiler" % "2.11.7",
@@ -40,6 +40,7 @@ libraryDependencies ++= Seq(
   "info.hupel" %% "libisabelle" % libisabelleVersion,
   "info.hupel" %% "libisabelle-setup" % libisabelleVersion,
   "info.hupel" %% "pide-2015" % libisabelleVersion,
+  "org.slf4j" % "slf4j-nop" % "1.7.13",
   "org.ow2.asm" % "asm-all" % "5.0.4",
   "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2"
 )
diff --git a/src/main/scala/leon/solvers/isabelle/Component.scala b/src/main/scala/leon/solvers/isabelle/Component.scala
index 3b75a8c64fb7a68db86fc30456a53d8df8e2626d..4f66f3a6da61dbfbe6be5e9c335dcb9633981bcd 100644
--- a/src/main/scala/leon/solvers/isabelle/Component.scala
+++ b/src/main/scala/leon/solvers/isabelle/Component.scala
@@ -8,6 +8,8 @@ import scala.concurrent.ExecutionContext.Implicits.global
 
 import leon._
 
+import edu.tum.cs.isabelle.setup._
+
 object Component extends LeonComponent {
 
   val name = "Isabelle"
@@ -16,13 +18,13 @@ object Component extends LeonComponent {
   val leonBase =
     Paths.get(Option(System.getProperty("leon.base")).getOrElse(".")).toAbsolutePath()
 
-  val isabelleBase =
-    leonBase.resolve("contrib").toAbsolutePath()
+  val platform =
+    Platform.guess.getOrElse(Platform.genericPlatform("generic", leonBase.resolve("contrib").toAbsolutePath()))
 
   val optBase = LeonStringOptionDef(
     name = "isabelle:base",
     description = "Base directory of the Isabelle installation",
-    default = isabelleBase.toString,
+    default = platform.setupStorage.toString,
     usageRhs = "path"
   )
 
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
index 4c76f386ba3c69ed8b0c25437894bda2734cd271..5856374e289d5f39c9669ec93ba6bef0e91e2693 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
@@ -51,15 +51,22 @@ object IsabelleEnvironment {
       }
     }.toList
 
-    val setup = Setup.detectSetup(base, version) match {
-      case Some(setup) => Future.successful { setup }
-      case None if !download =>
+    val home = base.resolve(s"Isabelle${version.identifier}")
+
+    val setup =
+      if (Files.isDirectory(home))
+        Future.successful { Setup(home, Component.platform, version) }
+      else if (!download)
         context.reporter.fatalError(s"No $version found at $base. Please install manually or set '${Component.optDownload.name}' flag to true.")
-      case _ =>
-        context.reporter.info(s"No $version found at $base")
-        context.reporter.info(s"Preparing $version environment ...")
-        Setup.installTo(Files.createDirectories(base).toRealPath(), version)
-    }
+      else
+        Component.platform match {
+          case o: OfficialPlatform =>
+            context.reporter.info(s"No $version found at $base")
+            context.reporter.info(s"Preparing $version environment ...")
+            Setup.install(o, version)
+          case _ =>
+            context.reporter.fatalError(s"No $version found at $base. Platform unsupported, please install manually.")
+        }
 
     val system = setup.flatMap { setup =>
       val env = Implementations.makeEnvironment(setup.home, classOf[edu.tum.cs.isabelle.impl.Environment])
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
index 40c754bc62b26a5bea51c9b00a84f5fb0d868efe..3b3e81860e38a1da24d0ce41f2d53a73a449732d 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
@@ -14,7 +14,6 @@ import leon.utils.Interruptible
 import leon.verification.VC
 
 import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.api.ProverResult
 
 class IsabelleSolver(val context: LeonContext, program: Program, types: Types, functions: Functions, system: System) extends Solver with Interruptible { self: TimeoutSolver =>
 
diff --git a/src/main/scala/leon/solvers/isabelle/package.scala b/src/main/scala/leon/solvers/isabelle/package.scala
index 421d64091da4f2c125dd25a2a52c611210e0e7c3..26f01fb5caa1afaae1a14d7d910ae9ff6045eef2 100644
--- a/src/main/scala/leon/solvers/isabelle/package.scala
+++ b/src/main/scala/leon/solvers/isabelle/package.scala
@@ -12,7 +12,6 @@ import leon.purescala.Expressions._
 import leon.verification.VC
 
 import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.api.ProverResult
 
 object `package` {