(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.

3 files changed, 18 insertions, 17 deletions

diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index be86b63..34873e4 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -132,9 +132,9 @@ Definition app:
   assumes "A: U i" "xs: List A" "ys: List A"
   shows "List A"
   apply (elim xs)
-  \<guillemotright> by (fact \<open>ys:_\<close>)
-  \<guillemotright> prems vars x _ rec
-    proof - show "x # rec: List A" by typechk qed
+    \<^item> by (fact \<open>ys:_\<close>)
+    \<^item> vars x _ rec
+      proof - show "x # rec: List A" by typechk qed
   done
 
 definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
@@ -169,8 +169,8 @@ Definition rev:
   assumes "A: U i" "xs: List A"
   shows "List A"
   apply (elim xs)
-  \<guillemotright> by (rule List_nil)
-  \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed
+    \<^item> by (rule List_nil)
+    \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed
   done
 
 definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 0ce534c..a2e1638 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -1,7 +1,7 @@
 chapter \<open>Maybe type\<close>
 
 theory Maybe
-imports More_Types
+imports Prelude
 
 begin
 
@@ -25,11 +25,10 @@ Definition MaybeInd:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "m: Maybe A"
   shows "C m"
-  supply assms[unfolded Maybe_def none_def some_def]
+  using assms[unfolded Maybe_def none_def some_def]
   apply (elim m)
-  \<guillemotright> unfolding Maybe_def .
-  \<guillemotright> by (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
-  \<guillemotright> by elim (rule \<open>_: C (inr _ _ _)\<close>)
+    apply (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
+    apply (elim, rule \<open>_: C (inr _ _ _)\<close>)
   done
 
 Lemma Maybe_comp_none:
@@ -39,8 +38,9 @@ Lemma Maybe_comp_none:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
   shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
-  supply assms[unfolded Maybe_def some_def none_def]
-  unfolding MaybeInd_def none_def by reduce
+  using assms
+  unfolding Maybe_def MaybeInd_def none_def some_def
+  by reduce
 
 Lemma Maybe_comp_some:
   assumes
@@ -50,8 +50,9 @@ Lemma Maybe_comp_some:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
   shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
-  supply assms[unfolded Maybe_def some_def none_def]
-  unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
+  using assms
+  unfolding Maybe_def MaybeInd_def none_def some_def
+  by reduce
 
 lemmas
   [form] = MaybeF and
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/Prelude.thy
index 55e6554..36f12d2 100644
--- a/spartan/lib/More_Types.thy
+++ b/spartan/lib/Prelude.thy
@@ -1,4 +1,4 @@
-theory More_Types
+theory Prelude
 imports Spartan
 
 begin
@@ -114,7 +114,7 @@ Lemma if_true:
     "b: C false"
   shows "ifelse C true a b \<equiv> a"
   unfolding ifelse_def true_def
-  supply assms[unfolded Bool_def true_def false_def]
+  using assms unfolding Bool_def true_def false_def
   by reduce
 
 Lemma if_false:
@@ -124,7 +124,7 @@ Lemma if_false:
     "b: C false"
   shows "ifelse C false a b \<equiv> b"
   unfolding ifelse_def false_def
-  supply assms[unfolded Bool_def true_def false_def]
+  using assms unfolding Bool_def true_def false_def
   by reduce
 
 lemmas