From 4f147cba894baa9e372e2b67211140b1a6f7b16c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 19 Jun 2020 12:41:54 +0200
Subject: reorganize

---
 ROOT | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

(limited to 'ROOT')

diff --git a/ROOT b/ROOT
index cc0badd..00d020a 100644
--- a/ROOT
+++ b/ROOT
@@ -1,18 +1,16 @@
 session Spartan_Core in "spartan/core" = Pure +
-  description "
-    Spartan type theory: a minimal dependent type theory based on intensional
+  description
+    "Spartan type theory: a minimal dependent type theory based on intensional
     Martin-Löf type theory with cumulative Russell-style universes, Pi types and
-    Sigma types. This session consists only of the very core theory files.
-  "
+    Sigma types."
   sessions
     "HOL-Eisbach"
   theories
     Spartan (global)
 
 session Spartan in spartan = Spartan_Core +
-  description "
-    Type theory based on Spartan, but with a few more bells and whistles.
-  "
+  description
+    "Dependent type theory based on Spartan."
   directories
     lib
   theories
@@ -21,15 +19,16 @@ session Spartan in spartan = Spartan_Core +
     List
 
 session HoTT in hott = Spartan +
-  description "
-    Homotopy type theory, following the development in
+  description
+    "Homotopy type theory, following the development in
       The Univalent Foundations Program,
       Homotopy Type Theory: Univalent Foundations of Mathematics,
       Institute for Advanced Study, (2013).
-      Available online at https://homotopytypetheory.org/book.
-  "
+      Available online at https://homotopytypetheory.org/book."
   theories
     Identity
     Equivalence
     Nat
     More_List
+    More_Nat
+
-- 
cgit v1.2.3