(FEAT) Term elaboration of assumption and goal statements.

  . spartan/core/goals.ML
  . spartan/core/elaboration.ML
  . spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.

1 files changed, 2 insertions, 4 deletions

diff --git a/ROOT b/ROOT
index 00d020a..b3aa520 100644
--- a/ROOT
+++ b/ROOT
@@ -14,7 +14,7 @@ session Spartan in spartan = Spartan_Core +
   directories
     lib
   theories
-    More_Types
+    Prelude
     Maybe
     List
 
@@ -29,6 +29,4 @@ session HoTT in hott = Spartan +
     Identity
     Equivalence
     Nat
-    More_List
-    More_Nat
-
+    "List+"