Brand-spanking new version using Spartan infrastructure

1 files changed, 6 insertions, 6 deletions

diff --git a/README.md b/README.md
index f254a8a..879b5d3 100644
--- a/README.md
+++ b/README.md
@@ -4,19 +4,19 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or
 
 ### Usage
 
-The default entry point for the logic is `HoTT`, import this to load everything else.
+Isabelle/HoTT is compatible with Isabelle2019.
+To use, add the Isabelle/HoTT folder path to `.isabelle/Isabelle2019/ROOTS` (on Mac/Linux/cygwin installations):
 
-You can also load theories selectively, in this case, importing `HoTT_Base` is required and `HoTT_Methods` is helpful.
+```
+echo <path/to/Isabelle/HoTT> >> ~/.isabelle/Isabelle2019/ROOTS
+```
 
 ### What (and why) is this?
 
 Isabelle/HoTT is a first attempt at bringing [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) to the [Isabelle](https://isabelle.in.tum.de/) interactive theorem prover.
-In its current state it is best viewed as a formalization of HoTT within Isabelle/Pure, largely following the development of the theory in the [Homotopy Type Theory book](https://homotopytypetheory.org/book/).
+It largely follows the development of the theory in the [Homotopy Type Theory book](https://homotopytypetheory.org/book/).
 
 Work is slowly ongoing to develop the logic into a fully-featured framework in which one can formulate and prove mathematical statements, in the style of the univalent foundations school.
 While Isabelle has provided support for object logics based on Martin-Löf type theory since the beginning, these have largely been ignored in favor of Isabelle/HOL.
 Thus this project is also an experiment in creating a viable framework, based on dependent type theory, inside the simple type theoretic foundations of Isabelle/Pure.
 
-### License
-
-GNU LGPLv3