From 32dc5b962b171a180568c1352a4a3301029605a1 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 29 Oct 2019 11:51:26 +0100
Subject: Update README.md

---
 README.md | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'README.md')

diff --git a/README.md b/README.md
index edc5399..a095173 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,9 @@
 
 An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/).
 
+**Update [15 Oct 2019]**: 
+Convenience and readability of formalizations in the library is taking a hit as we move to the limits of the currently available functionality in Isabelle, so for the moment development has moved [here](https://github.com/jaycech3n/Isabelle-Spartan), in order to first build more necessary automation and improve the framework.
+
 ### Usage
 
 The default entry point for the logic is `HoTT`, import this to load everything else.
@@ -16,7 +19,8 @@ In its current state it is best viewed as a formalization of HoTT within Isabell
 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.
-**Update (15 Oct 2019)**: Framework development currently [here](https://github.com/jaycech3n/Isabelle-Spartan).
+
+A writeup of some theoretical considerations in this implementation is in my [Masters thesis](https://joshchen.io/assets/ms_thesis_submitted.pdf).
 
 ### License
 
-- 
cgit v1.2.3