reorganize

1 files changed, 10 insertions, 11 deletions

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
+