diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 58bbf387e15f357b463b2321b735282df397fe9f..0000000000000000000000000000000000000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "unmanaged/isabelle/protocol"]
-	path = unmanaged/isabelle/protocol
-	url = https://github.com/larsrh/libisabelle-protocol.git
diff --git a/ROOTS b/ROOTS
deleted file mode 100644
index 011708995db7c4dd771f19c5d366d74059e0abde..0000000000000000000000000000000000000000
--- a/ROOTS
+++ /dev/null
@@ -1,2 +0,0 @@
-unmanaged/isabelle/protocol
-src/main/isabelle
diff --git a/build.sbt b/build.sbt
index cafc0af35392aa20dac26ea2cea2cc31af77a2f5..ee6223e2bc8eac53a1201269f605a4cc8681739d 100644
--- a/build.sbt
+++ b/build.sbt
@@ -28,10 +28,11 @@ if(System.getProperty("sun.arch.data.model") == "64") {
 
 resolvers ++= Seq(
   "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/",
-  "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
+  "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots",
+  "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases"
 )
 
-val libisabelleVersion = "0.2"
+val libisabelleVersion = "0.3"
 
 libraryDependencies ++= Seq(
   "org.scala-lang" % "scala-compiler" % "2.11.7",
@@ -39,7 +40,6 @@ libraryDependencies ++= Seq(
   "com.typesafe.akka" %% "akka-actor" % "2.3.4",
   "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",
@@ -88,13 +88,11 @@ script := {
       s.log.info("Generating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
     }
     val paths = (res.getAbsolutePath +: out.getAbsolutePath +: cps.map(_.data.absolutePath)).mkString(System.getProperty("path.separator"))
-    val base = baseDirectory.value.getAbsolutePath
     IO.write(f, s"""|#!/bin/bash --posix
                     |
                     |SCALACLASSPATH="$paths"
-                    |BASEDIRECTORY="$base"
                     |
-                    |java -Xmx2G -Xms512M -Xss64M -classpath "$${SCALACLASSPATH}" -Dleon.base="$${BASEDIRECTORY}" -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath "$${SCALACLASSPATH}" leon.Main $$@ 2>&1 | tee -i last.log
+                    |java -Xmx2G -Xms512M -Xss64M -classpath "$${SCALACLASSPATH}" -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath "$${SCALACLASSPATH}" leon.Main $$@ 2>&1 | tee -i last.log
                     |""".stripMargin)
     f.setExecutable(true)
   } catch {
diff --git a/project/plugins.sbt b/project/plugins.sbt
index 9a94578c3c5cb3741993e490723649b67eb71441..fe91723924812684dbbbe5c04a401a120b339a0d 100644
--- a/project/plugins.sbt
+++ b/project/plugins.sbt
@@ -1 +1,3 @@
 addSbtPlugin("com.typesafe.sbt" % "sbt-site" % "0.8.1")
+
+addSbtPlugin("info.hupel" % "sbt-libisabelle" % "0.1")
diff --git a/src/main/isabelle/ROOT b/src/main/isabelle/ROOT
index 5c659007c62c6eaf46ea0a690c2e5aad05574bf8..d95bef0c4a3bcacb7ab56a1767280e54a749e285 100644
--- a/src/main/isabelle/ROOT
+++ b/src/main/isabelle/ROOT
@@ -1,4 +1,4 @@
-session Leon_Deps = "HOL-Protocol2015" +
+session Leon_Deps = "HOL-Protocol" +
   theories
     "~~/src/HOL/Word/Word"
     "~~/src/HOL/Library/Simps_Case_Conv"
diff --git a/src/main/scala/leon/solvers/isabelle/Component.scala b/src/main/scala/leon/solvers/isabelle/Component.scala
index 55e2eef1ed068a63d9e5ccab66dbf0ca57dfeb49..463ed8478b62fb3753cf5522e14b485e7baccc58 100644
--- a/src/main/scala/leon/solvers/isabelle/Component.scala
+++ b/src/main/scala/leon/solvers/isabelle/Component.scala
@@ -17,30 +17,8 @@ object Component extends LeonComponent {
   val name = "Isabelle"
   val description = "Isabelle solver"
 
-  val leonBase =
-    Paths.get(Option(System.getProperty("leon.base")).getOrElse(".")).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 = platform.setupStorage.toString,
-    usageRhs = "path"
-  )
-
-  val optDownload = LeonFlagOptionDef(
-    name = "isabelle:download",
-    description = "Automatic download of Isabelle",
-    default = false
-  )
-
-  val optBuild = LeonFlagOptionDef(
-    name = "isabelle:build",
-    description = "Automatic build of Isabelle/Leon",
-    default = true
-  )
+  def platform =
+    Platform.guess.getOrElse(sys.error("Unknown platform; can't run Isabelle here"))
 
   val optMapping = LeonFlagOptionDef(
     name = "isabelle:mapping",
@@ -62,6 +40,6 @@ object Component extends LeonComponent {
   )
 
   override val definedOptions: Set[LeonOptionDef[Any]] =
-    Set(optBase, optDownload, optBuild, optMapping, optDump, optStrict)
+    Set(optMapping, optDump, optStrict)
 
 }
diff --git a/src/main/scala/leon/solvers/isabelle/Functions.scala b/src/main/scala/leon/solvers/isabelle/Functions.scala
index 9e221e988f7e0671ccbe9ac21a8b0c2acf8c24e2..a258fd1cd83813a05c0303af2d067f1e1f181f21 100644
--- a/src/main/scala/leon/solvers/isabelle/Functions.scala
+++ b/src/main/scala/leon/solvers/isabelle/Functions.scala
@@ -14,6 +14,7 @@ import leon.purescala.Types._
 import leon.utils._
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
 
 final class Functions(context: LeonContext, program: Program, types: Types, funs: List[FunDef], system: System)(implicit ec: ExecutionContext) {
 
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
index 944a2e2490db8e3745228a0f5ac0864592c427ff..8f762612fd91b062a99d95d799e948da45747c36 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
@@ -28,9 +28,6 @@ object IsabelleEnvironment {
 
   def apply(context: LeonContext, program: Program): Future[IsabelleEnvironment] = {
     val version = Version(isabelleVersion)
-    val base = Paths.get(context.findOptionOrDefault(Component.optBase))
-    val download = context.findOptionOrDefault(Component.optDownload)
-    val build = context.findOptionOrDefault(Component.optBuild)
     val dump = context.findOptionOrDefault(Component.optDump)
     val strict = context.findOptionOrDefault(Component.optStrict)
 
@@ -53,35 +50,21 @@ object IsabelleEnvironment {
       }
     }.toList
 
-    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.")
-      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.")
-        }
+    context.reporter.info(s"Preparing Isabelle setup (this might take a while) ...")
+    val setup = Setup.defaultSetup(version)
 
     val system = setup.flatMap { setup =>
-      val env = Implementations.makeEnvironment(setup.home, classOf[edu.tum.cs.isabelle.impl.Environment])
-      val config = Configuration.fromPath(Component.leonBase, "Leon")
+      val resources = Resources.dumpIsabelleResources()
+      val config = resources.makeConfiguration(Nil, "Leon")
 
-      if (build) {
+      setup.makeEnvironment.flatMap { env =>
         context.reporter.info(s"Building session ...")
         if (!System.build(env, config))
           context.reporter.internalError("Build failed")
-      }
 
-      context.reporter.info(s"Starting $version instance ...")
-      System.create(env, config)
+        context.reporter.info(s"Starting $version instance ...")
+        System.create(env, config)
+      }
     }
 
     val thy = system.flatMap { system =>
@@ -126,10 +109,12 @@ object IsabelleEnvironment {
 
     functions.flatMap(_.data).foreach { _ =>
       if (dump.isEmpty)
-        system.flatMap(_.invoke(Report)(())).assertSuccess(context).foreach { report =>
-          context.reporter.debug(s"Report for $theory ...")
-          report.foreach { case (key, value) =>
-            context.reporter.debug(s"$key: ${canonicalizeOutput(value)}")
+        system.foreach { sys =>
+          sys.invoke(Report)(()).assertSuccess(context).foreach { report =>
+            context.reporter.debug(s"Report for $theory ...")
+            report.foreach { case (key, value) =>
+              context.reporter.debug(s"$key: ${canonicalizeOutput(sys, value)}")
+            }
           }
         }
       else
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
index 9bf81247d5a6648c1cdb10eae23b1d8d30791f3b..a6b52a3211e0729b78d62bce27281d98905af5f2 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
@@ -16,6 +16,7 @@ import leon.utils.Interruptible
 import leon.verification.VC
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
 
 class IsabelleSolver(val context: LeonContext, program: Program, types: Types, functions: Functions, system: System) extends Solver with Interruptible { self: TimeoutSolver =>
 
@@ -49,7 +50,7 @@ class IsabelleSolver(val context: LeonContext, program: Program, types: Types, f
   def check: Option[Boolean] = {
     val verdict = sequencePending().flatMapC { ts =>
       Future.traverse(ts)(system.invoke(Pretty)(_).assertSuccess(context)).foreach { strs =>
-        context.reporter.debug(s"Attempting to prove disjunction of ${canonicalizeOutput(strs.mkString(", "))}")
+        context.reporter.debug(s"Attempting to prove disjunction of ${canonicalizeOutput(system, strs.mkString(", "))}")
       }
 
       system.cancellableInvoke(Prove)((ts, method))
@@ -59,7 +60,7 @@ class IsabelleSolver(val context: LeonContext, program: Program, types: Types, f
     try {
       Await.result(verdict.future.assertSuccess(context), timeout) match {
         case Some(thm) =>
-          context.reporter.debug(s"Proved theorem: ${canonicalizeOutput(thm)}")
+          context.reporter.debug(s"Proved theorem: ${canonicalizeOutput(system, thm)}")
           Some(false)
         case None =>
           None
diff --git a/src/main/scala/leon/solvers/isabelle/Translator.scala b/src/main/scala/leon/solvers/isabelle/Translator.scala
index 79c4cfea7c520383a3aaa1f05b824f9535bca504..3a0734726f0a2118bf3621fd1b9da35aa31b8f2e 100644
--- a/src/main/scala/leon/solvers/isabelle/Translator.scala
+++ b/src/main/scala/leon/solvers/isabelle/Translator.scala
@@ -14,6 +14,7 @@ import leon.purescala.Types._
 import leon.utils._
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
 
 final class Translator(context: LeonContext, program: Program, types: Types, system: System)(implicit ec: ExecutionContext) {
 
diff --git a/src/main/scala/leon/solvers/isabelle/Types.scala b/src/main/scala/leon/solvers/isabelle/Types.scala
index 268a1b7885d10867e6284042716b1abdbe95175a..3847d80c5831fd84c1fc342c8fe8e9d61429c6bd 100644
--- a/src/main/scala/leon/solvers/isabelle/Types.scala
+++ b/src/main/scala/leon/solvers/isabelle/Types.scala
@@ -12,6 +12,7 @@ import leon.purescala.Expressions._
 import leon.purescala.Types._
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.pure._
 
 case class Constructor(term: Term, disc: Term, sels: Map[ValDef, Term])
 case class Datatype(typ: String, constructors: Map[CaseClassDef, Constructor])
diff --git a/src/main/scala/leon/solvers/isabelle/package.scala b/src/main/scala/leon/solvers/isabelle/package.scala
index 49046965365633b0632534d1be2661b1c7fac9c6..c06f4f59b9f1d3eb11bf924d1812c8eb1e30dc8b 100644
--- a/src/main/scala/leon/solvers/isabelle/package.scala
+++ b/src/main/scala/leon/solvers/isabelle/package.scala
@@ -14,6 +14,10 @@ import leon.purescala.Expressions._
 import leon.verification.VC
 
 import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.api.Environment
+import edu.tum.cs.isabelle.pure.{Expr => _, _}
+
+import shapeless.tag
 
 object `package` {
 
@@ -108,10 +112,11 @@ object `package` {
     }
   }
 
-  def canonicalizeOutput(str: String) =
-    // FIXME expose this via libisabelle
+  def canonicalizeOutput(system: System, str: String) = {
     // FIXME use this everywhere
-    isabelle.Symbol.decode("""\s+""".r.replaceAllIn(str, " "))
+    val raw = """\s+""".r.replaceAllIn(str, " ")
+    system.env.decode(tag[Environment.Raw].apply(raw))
+  }
 
   val Prove = Operation.implicitly[(List[Term], Option[String]), Option[String]]("prove")
   val Pretty = Operation.implicitly[Term, String]("pretty")
diff --git a/src/sphinx/isabelle.rst b/src/sphinx/isabelle.rst
index c48fa16ebfe37d1ddce0400c56ffdea99fb2ba29..a375ccb4302926d839b2b8015b7af09d34b866cf 100644
--- a/src/sphinx/isabelle.rst
+++ b/src/sphinx/isabelle.rst
@@ -28,20 +28,10 @@ verification.
 Installation
 ------------
 
-You can obtain a copy of Isabelle for your operating system at `its website
-<https://isabelle.in.tum.de/>`_, then follow the `installation instructions
-<https://isabelle.in.tum.de/installation.html>`_. The installation path needs
-to be passed to Leon via the ``--isabelle:base`` command line option. (The path
-will end in ``Isabelle2015``. Depending on your operating system, this folder
-might be some levels into the installation tree.)
-
-On Linux, you can skip this step. Leon is able to download and install Isabelle
-itself. During the first start, you just need to pass the command line option
-``--isabelle:download=true``. You may specify ``--isabelle:base``, but don't
-have to.
-
-Additionally, you need to instruct Git to fetch all the referenced repositories
-via ``git submodule update --init --recursive``.
+You don't have to obtain a copy of Isabelle. Leon is able to download and
+install Isabelle itself. The installation happens in the appropriate folder for
+your operating system, e.g. ``%APPDATA%`` under Windows or ``$HOME/.local``
+under Linux.
 
 
 Basic usage
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
index a5be01e35269e12864cd6716947727209497b337..38f18d0aef81eea7dd1006c92fda59f170b3f25e 100644
--- a/src/sphinx/options.rst
+++ b/src/sphinx/options.rst
@@ -313,27 +313,6 @@ CVC4 Solver
 Isabelle
 ********
 
-* ``--isabelle:base=<path>``
-
-  Specify the installation directory of Isabelle. In Isabelle-parlance, this is
-  called ``$ISABELLE_HOME``. It will have the form ``/path/to/Isabelle2015``.
-  When no Isabelle installation can be found there, the system suggests to
-  enable the ``download`` option.
-
-* ``--isabelle:build``
-
-  Flag to indicate that during the start-up of Leon, Isabelle should
-  automatically build all required library sources. This is on by default, and
-  should usually be left on. Building only happens when some dependencies
-  changed and subsequent runs of Leon don't rebuild the library. However, even
-  if nothing is build, it still requires the system a couple of seconds to
-  figure that out.
-
-* ``--isabelle:download``
-
-  If necessary, perform a full system bootstrap by downloading and unpacking a
-  copy of Isabelle. Off by default. Only supported under Linux.
-
 * ``--isabelle:dump=<path>``
 
   Makes the system write theory files containing the translated definitions
diff --git a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala b/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
index bf4acc20261f11e6c64f4be5ce806ed21a6f8707..ba2ce427d4f052dac39a07a025ae298fb0e66156 100644
--- a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
+++ b/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
@@ -29,7 +29,7 @@ class IsabelleLibrarySuite extends LeonRegressionSuite {
   test("Define the library") {
     val pipeline = ExtractionPhase andThen new PreprocessingPhase andThen IsabelleNoopPhase
 
-    val ctx = Main.processOptions(Seq("--isabelle:download=true", "--functions=_")).copy(reporter = new TestSilentReporter())
+    val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
 
     pipeline.run(ctx, Nil)
   }
diff --git a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala b/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
index d8a5ba46f202d5900d1babc6bf510a530ac105e6..7540c296df2b26ac93a6e193466d9563602c591b 100644
--- a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
+++ b/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
@@ -9,6 +9,6 @@ class IsabelleVerificationSuite extends VerificationSuite {
   val testDir = "regression/verification/isabelle/"
   override val isabelle = true
 
-  val optionVariants: List[List[String]] = List(List("--isabelle:download=true", "--solvers=isabelle"))
+  val optionVariants: List[List[String]] = List(List("--solvers=isabelle"))
 
 }
diff --git a/unmanaged/isabelle/protocol b/unmanaged/isabelle/protocol
deleted file mode 160000
index c33db5fef8af6548c494705e55e6b56e976a10a9..0000000000000000000000000000000000000000
--- a/unmanaged/isabelle/protocol
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit c33db5fef8af6548c494705e55e6b56e976a10a9