rename things + some small changes

17 files changed, 0 insertions, 3610 deletions

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
deleted file mode 100644
index 5046b6a..0000000
--- a/spartan/core/Spartan.thy
+++ /dev/null
@@ -1,571 +0,0 @@
-text \<open>Spartan type theory\<close>
-
-theory Spartan
-imports
-  Pure
-  "HOL-Eisbach.Eisbach"
-  "HOL-Eisbach.Eisbach_Tools"
-keywords
-  "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and
-  "assuming" :: prf_asm % "proof" and
-  "focus" "\<^item>" "\<^enum>" "\<circ>" "\<diamondop>" "~" :: prf_script_goal % "proof" and
-  "calc" "print_coercions" :: thy_decl and
-  "rhs" "def" "vars" :: quasi_command
-
-begin
-
-section \<open>Notation\<close>
-
-declare [[eta_contract=false]]
-
-text \<open>
-Rebind notation for meta-lambdas since we want to use \<open>\<lambda>\<close> for the object
-lambdas. Metafunctions now use the binder \<open>fn\<close>.
-\<close>
-setup \<open>
-let
-  val typ = Simple_Syntax.read_typ
-  fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range)
-in
-  Sign.del_syntax (Print_Mode.ASCII, true)
-    [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3))]
-  #> Sign.del_syntax Syntax.mode_default
-    [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3))]
-  #> Sign.add_syntax Syntax.mode_default
-    [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))]
-end
-\<close>
-
-syntax "_app" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
-translations "a $ b" \<rightharpoonup> "a (b)"
-
-abbreviation (input) K where "K x \<equiv> fn _. x"
-
-
-section \<open>Metalogic\<close>
-
-text \<open>
-HOAS embedding of dependent type theory: metatype of expressions, and typing
-judgment.
-\<close>
-
-typedecl o
-
-consts has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
-
-
-section \<open>Axioms\<close>
-
-subsection \<open>Universes\<close>
-
-text \<open>\<omega>-many cumulative Russell universes.\<close>
-
-typedecl lvl
-
-axiomatization
-  O  :: \<open>lvl\<close> and
-  S  :: \<open>lvl \<Rightarrow> lvl\<close> and
-  lt :: \<open>lvl \<Rightarrow> lvl \<Rightarrow> prop\<close> (infix "<" 900)
-  where
-  O_min: "O < S i" and
-  lt_S: "i < S i" and
-  lt_trans: "i < j \<Longrightarrow> j < k \<Longrightarrow> i < k"
-
-axiomatization U :: \<open>lvl \<Rightarrow> o\<close> where
-  Ui_in_Uj: "i < j \<Longrightarrow> U i: U j" and
-  U_cumul: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j"
-
-lemma Ui_in_USi:
-  "U i: U (S i)"
-  by (rule Ui_in_Uj, rule lt_S)
-
-lemma U_lift:
-  "A: U i \<Longrightarrow> A: U (S i)"
-  by (erule U_cumul, rule lt_S)
-
-subsection \<open>\<Prod>-type\<close>
-
-axiomatization
-  Pi  :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and
-  lam :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and
-  app :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("(1_ `_)" [120, 121] 120)
-
-syntax
-  "_Pi"   :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Prod>_: _./ _)" 30)
-  "_Pi2"  :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
-  "_lam"  :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_: _./ _)" 30)
-  "_lam2" :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
-translations
-  "\<Prod>x xs: A. B" \<rightharpoonup> "CONST Pi A (fn x. _Pi2 xs A B)"
-  "_Pi2 x A B"  \<rightharpoonup> "\<Prod>x: A. B"
-  "\<Prod>x: A. B"    \<rightleftharpoons> "CONST Pi A (fn x. B)"
-  "\<lambda>x xs: A. b" \<rightharpoonup> "CONST lam A (fn x. _lam2 xs A b)"
-  "_lam2 x A b" \<rightharpoonup> "\<lambda>x: A. b"
-  "\<lambda>x: A. b"    \<rightleftharpoons> "CONST lam A (fn x. b)"
-
-abbreviation Fn (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B"
-
-axiomatization where
-  PiF: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and
-
-  PiI: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and
-
-  PiE: "\<lbrakk>f: \<Prod>x: A. B x; a: A\<rbrakk> \<Longrightarrow> f `a: B a" and
-
-  beta: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> (\<lambda>x: A. b x) `a \<equiv> b a" and
-
-  eta: "f: \<Prod>x: A. B x \<Longrightarrow> \<lambda>x: A. f `x \<equiv> f" and
-
-  Pi_cong: "\<lbrakk>
-    \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x;
-    A: U i;
-    \<And>x. x: A \<Longrightarrow> B x: U j;
-    \<And>x. x: A \<Longrightarrow> B' x: U j
-    \<rbrakk> \<Longrightarrow> \<Prod>x: A. B x \<equiv> \<Prod>x: A. B' x" and
-
-  lam_cong: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x"
-
-subsection \<open>\<Sum>-type\<close>
-
-axiomatization
-  Sig    :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and
-  pair   :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("(2<_,/ _>)") and
-  SigInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
-
-syntax "_Sum" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Sum>_: _./ _)" 20)
-
-translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (fn x. B)"
-
-abbreviation Prod (infixl "\<times>" 60)
-  where "A \<times> B \<equiv> \<Sum>_: A. B"
-
-abbreviation "and" (infixl "\<and>" 60)
-  where "A \<and> B \<equiv> A \<times> B"
-
-axiomatization where
-  SigF: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and
-
-  SigI: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a, b>: \<Sum>x: A. B x" and
-
-  SigE: "\<lbrakk>
-    p: \<Sum>x: A. B x;
-    A: U i;
-    \<And>x. x : A \<Longrightarrow> B x: U j;
-    \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U k;
-    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>
-    \<rbrakk> \<Longrightarrow> SigInd A (fn x. B x) (fn p. C p) f p: C p" and
-
-  Sig_comp: "\<lbrakk>
-    a: A;
-    b: B a;
-    \<And>x. x: A \<Longrightarrow> B x: U i;
-    \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i;
-    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>
-    \<rbrakk> \<Longrightarrow> SigInd A (fn x. B x) (fn p. C p) f <a, b> \<equiv> f a b" and
-
-  Sig_cong: "\<lbrakk>
-    \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x;
-    A: U i;
-    \<And>x. x : A \<Longrightarrow> B x: U j;
-    \<And>x. x : A \<Longrightarrow> B' x: U j
-    \<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x"
-
-
-section \<open>Type checking & inference\<close>
-
-ML_file \<open>lib.ML\<close>
-ML_file \<open>context_facts.ML\<close>
-ML_file \<open>context_tactical.ML\<close>
-
-\<comment> \<open>Rule attributes for the typechecker\<close>
-named_theorems form and intr and comp
-
-\<comment> \<open>Elimination/induction automation and the `elim` attribute\<close>
-ML_file \<open>elimination.ML\<close>
-
-lemmas
-  [form] = PiF SigF and
-  [intr] = PiI SigI and
-  [elim ?f] = PiE and
-  [elim ?p] = SigE and
-  [comp] = beta Sig_comp and
-  [cong] = Pi_cong lam_cong Sig_cong
-
-\<comment> \<open>Subsumption rule\<close>
-lemma sub:
-  assumes "a: A" "A \<equiv> A'"
-  shows "a: A'"
-  using assms by simp
-
-\<comment> \<open>Basic rewriting of computational equality\<close>
-ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
-ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
-
-\<comment> \<open>Term normalization, type checking & inference\<close>
-ML_file \<open>types.ML\<close>
-
-method_setup typechk =
-  \<open>Scan.succeed (K (CONTEXT_METHOD (
-    CHEADGOAL o Types.check_infer)))\<close>
-
-method_setup known =
-  \<open>Scan.succeed (K (CONTEXT_METHOD (
-    CHEADGOAL o Types.known_ctac)))\<close>
-
-setup \<open>
-let val typechk = fn ctxt =>
-  NO_CONTEXT_TACTIC ctxt o Types.check_infer
-    (Simplifier.prems_of ctxt @ Context_Facts.known ctxt)
-in
-  map_theory_simpset (fn ctxt => ctxt
-    addSolver (mk_solver "" typechk))
-end
-\<close>
-
-
-section \<open>Statements and goals\<close>
-
-ML_file \<open>focus.ML\<close>
-ML_file \<open>elaboration.ML\<close>
-ML_file \<open>elaborated_statement.ML\<close>
-ML_file \<open>goals.ML\<close>
-
-
-section \<open>Proof methods\<close>
-
-named_theorems intro \<comment> \<open>Logical introduction rules\<close>
-
-lemmas [intro] = PiI[rotated] SigI
-
-\<comment> \<open>Case reasoning rules\<close>
-ML_file \<open>cases.ML\<close>
-
-ML_file \<open>tactics.ML\<close>
-
-method_setup rule =
-  \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS 0 (rule_ctac ths))))\<close>
-
-method_setup dest =
-  \<open>Scan.lift (Scan.option (Args.parens Parse.nat))
-    -- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD (
-      CHEADGOAL o SIDE_CONDS 0 (dest_ctac n_opt ths))))\<close>
-
-method_setup intro =
-  \<open>Scan.succeed (K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS 0 intro_ctac)))\<close>
-
-method_setup intros =
-  \<open>Scan.lift (Scan.option Parse.nat) >> (fn n_opt =>
-    K (CONTEXT_METHOD (fn facts =>
-      case n_opt of
-        SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))
-      | NONE => CCHANGED (CREPEAT (CCHANGED (
-          CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)))))))\<close>
-
-method_setup elim =
-  \<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS 0 (elim_ctac tms))))\<close>
-
-method_setup cases =
-  \<open>Args.term >> (fn tm => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS 0 (cases_ctac tm))))\<close>
-
-method elims = elim+
-method facts = fact+
-
-
-subsection \<open>Reflexivity\<close>
-
-named_theorems refl
-method refl = (rule refl)
-
-
-subsection \<open>Trivial proofs (modulo automatic discharge of side conditions)\<close>
-
-method_setup this =
-  \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts =>
-    CHEADGOAL (SIDE_CONDS 0
-      (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts))
-      facts))))\<close>
-
-
-subsection \<open>Rewriting\<close>
-
-consts compute_hole :: "'a::{}"  ("\<hole>")
-
-lemma eta_expand:
-  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
-  shows "f \<equiv> fn x. f x" .
-
-lemma rewr_imp:
-  assumes "PROP A \<equiv> PROP B"
-  shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
-  apply (Pure.rule Pure.equal_intr_rule)
-  apply (drule equal_elim_rule2[OF assms]; assumption)
-  apply (drule equal_elim_rule1[OF assms]; assumption)
-  done
-
-lemma imp_cong_eq:
-  "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
-    ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
-  apply (Pure.intro Pure.equal_intr_rule)
-    apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2;
-      assumption)+
-    apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
-  done
-
-ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
-ML_file \<open>comp.ML\<close>
-
-\<comment> \<open>\<open>compute\<close> simplifies terms via computational equalities\<close>
-method compute uses add =
-  changed \<open>repeat_new \<open>(simp add: comp add | subst comp); typechk?\<close>\<close>
-
-
-subsection \<open>Calculational reasoning\<close>
-
-consts "rhs" :: \<open>'a\<close> ("..")
-
-ML_file \<open>calc.ML\<close>
-
-
-section \<open>Implicits\<close>
-
-text \<open>
-  \<open>{}\<close> is used to mark implicit arguments in definitions, while \<open>?\<close> is expanded
-  immediately for elaboration in statements.
-\<close>
-
-consts
-  iarg :: \<open>'a\<close> ("{}")
-  hole :: \<open>'b\<close> ("?")
-
-ML_file \<open>implicits.ML\<close>
-
-attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
-
-ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\<close>
-
-text \<open>Automatically insert inhabitation judgments where needed:\<close>
-
-syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
-translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
-
-
-subsection \<open>Implicit lambdas\<close>
-
-definition lam_i where [implicit]: "lam_i f \<equiv> lam {} f"
-
-syntax
-  "_lam_i"  :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_./ _)" 30)
-  "_lam_i2" :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close>
-translations
-  "\<lambda>x xs. b" \<rightharpoonup> "CONST lam_i (fn x. _lam_i2 xs b)"
-  "_lam_i2 x b" \<rightharpoonup> "\<lambda>x. b"
-  "\<lambda>x. b"    \<rightleftharpoons> "CONST lam_i (fn x. b)"
-
-translations "\<lambda>x. b" \<leftharpoondown> "\<lambda>x: A. b"
-
-
-section \<open>Lambda coercion\<close>
-
-\<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
-abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>
-  where "lambda f \<equiv> fn x. f `x"
-
-ML_file \<open>~~/src/Tools/subtyping.ML\<close>
-declare [[coercion_enabled, coercion lambda]]
-
-translations "f x" \<leftharpoondown> "f `x"
-
-
-section \<open>Functions\<close>
-
-Lemma eta_exp:
-  assumes "f: \<Prod>x: A. B x"
-  shows "f \<equiv> \<lambda>x: A. f x"
-  by (rule eta[symmetric])
-
-Lemma refine_codomain:
-  assumes
-    "A: U i"
-    "f: \<Prod>x: A. B x"
-    "\<And>x. x: A \<Longrightarrow> f `x: C x"
-  shows "f: \<Prod>x: A. C x"
-  by (comp eta_exp)
-
-Lemma lift_universe_codomain:
-  assumes "A: U i" "f: A \<rightarrow> U j"
-  shows "f: A \<rightarrow> U (S j)"
-  using U_lift
-  by (rule refine_codomain)
-
-subsection \<open>Function composition\<close>
-
-definition "funcomp A g f \<equiv> \<lambda>x: A. g `(f `x)"
-
-syntax
-  "_funcomp" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ \<circ>\<^bsub>_\<^esub>/ _)" [111, 0, 110] 110)
-translations
-  "g \<circ>\<^bsub>A\<^esub> f" \<rightleftharpoons> "CONST funcomp A g f"
-
-Lemma funcompI [type]:
-  assumes
-    "A: U i"
-    "B: U i"
-    "\<And>x. x: B \<Longrightarrow> C x: U i"
-    "f: A \<rightarrow> B"
-    "g: \<Prod>x: B. C x"
-  shows
-    "g \<circ>\<^bsub>A\<^esub> f: \<Prod>x: A. C (f x)"
-  unfolding funcomp_def by typechk
-
-Lemma funcomp_assoc [comp]:
-  assumes
-    "A: U i"
-    "f: A \<rightarrow> B"
-    "g: B \<rightarrow> C"
-    "h: \<Prod>x: C. D x"
-  shows
-    "(h \<circ>\<^bsub>B\<^esub> g) \<circ>\<^bsub>A\<^esub> f \<equiv> h \<circ>\<^bsub>A\<^esub> g \<circ>\<^bsub>A\<^esub> f"
-  unfolding funcomp_def by compute
-
-Lemma funcomp_lambda_comp [comp]:
-  assumes
-    "A: U i"
-    "\<And>x. x: A \<Longrightarrow> b x: B"
-    "\<And>x. x: B \<Longrightarrow> c x: C x"
-  shows
-    "(\<lambda>x: B. c x) \<circ>\<^bsub>A\<^esub> (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)"
-  unfolding funcomp_def by compute
-
-Lemma funcomp_apply_comp [comp]:
-  assumes
-    "A: U i" "B: U i" "\<And>x y. x: B \<Longrightarrow> C x: U i"
-    "f: A \<rightarrow> B" "g: \<Prod>x: B. C x"
-    "x: A"
-  shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
-  unfolding funcomp_def by compute
-
-subsection \<open>Notation\<close>
-
-definition funcomp_i (infixr "\<circ>" 120)
-  where [implicit]: "funcomp_i g f \<equiv> g \<circ>\<^bsub>{}\<^esub> f"
-
-translations "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
-
-subsection \<open>Identity function\<close>
-
-abbreviation id where "id A \<equiv> \<lambda>x: A. x"
-
-lemma
-  id_type [type]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
-  id_comp [comp]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close>
-  by compute+
-
-Lemma id_left [comp]:
-  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
-  shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f"
-  by (comp eta_exp[of f]) (compute, rule eta)
-
-Lemma id_right [comp]:
-  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
-  shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
-  by (comp eta_exp[of f]) (compute, rule eta)
-
-lemma id_U [type]:
-  "id (U i): U i \<rightarrow> U i"
-  using Ui_in_USi by typechk
-
-
-section \<open>Pairs\<close>
-
-definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn _. A) (fn x y. x) p"
-definition "snd A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn p. B (fst A B p)) (fn x y. y) p"
-
-Lemma fst_type [type]:
-  assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
-  shows "fst A B: (\<Sum>x: A. B x) \<rightarrow> A"
-  unfolding fst_def by typechk
-
-Lemma fst_comp [comp]:
-  assumes
-    "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
-  shows "fst A B <a, b> \<equiv> a"
-  unfolding fst_def by compute
-
-Lemma snd_type [type]:
-  assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
-  shows "snd A B: \<Prod>p: \<Sum>x: A. B x. B (fst A B p)"
-  unfolding snd_def by typechk
-
-Lemma snd_comp [comp]:
-  assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
-  shows "snd A B <a, b> \<equiv> b"
-  unfolding snd_def by compute
-
-subsection \<open>Notation\<close>
-
-definition fst_i ("fst")
-  where [implicit]: "fst \<equiv> Spartan.fst {} {}"
-
-definition snd_i ("snd")
-  where [implicit]: "snd \<equiv> Spartan.snd {} {}"
-
-translations
-  "fst" \<leftharpoondown> "CONST Spartan.fst A B"
-  "snd" \<leftharpoondown> "CONST Spartan.snd A B"
-
-subsection \<open>Projections\<close>
-
-Lemma fst [type]:
-  assumes
-    "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
-    "p: \<Sum>x: A. B x"
-  shows "fst p: A"
-  by typechk
-
-Lemma snd [type]:
-  assumes
-    "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
-    "p: \<Sum>x: A. B x"
-  shows "snd p: B (fst p)"
-  by typechk
-
-method fst for p::o = rule fst[where ?p=p]
-method snd for p::o = rule snd[where ?p=p]
-
-text \<open>Double projections:\<close>
-
-definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.snd {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.snd {} {} p)"
-
-translations
-  "CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
-  "CONST p\<^sub>1\<^sub>2 p" \<leftharpoondown> "snd (fst p)"
-  "CONST p\<^sub>2\<^sub>1 p" \<leftharpoondown> "fst (snd p)"
-  "CONST p\<^sub>2\<^sub>2 p" \<leftharpoondown> "snd (snd p)"
-
-Lemma (def) distribute_Sig:
-  assumes
-    "A: U i"
-    "\<And>x. x: A \<Longrightarrow> B x: U i"
-    "\<And>x. x: A \<Longrightarrow> C x: U i"
-    "p: \<Sum>x: A. B x \<times> C x"
-  shows "(\<Sum>x: A. B x) \<times> (\<Sum>x: A. C x)"
-  proof intro
-    have "fst p: A" and "snd p: B (fst p) \<times> C (fst p)"
-      by typechk+
-    thus "<fst p, fst (snd p)>: \<Sum>x: A. B x"
-     and "<fst p, snd (snd p)>: \<Sum>x: A. C x"
-      by typechk+
-  qed
-
-
-end
diff --git a/spartan/core/calc.ML b/spartan/core/calc.ML
deleted file mode 100644
index 67dc7fc..0000000
--- a/spartan/core/calc.ML
+++ /dev/null
@@ -1,87 +0,0 @@
-structure Calc = struct
-
-(* Calculational type context data
-
-A "calculational" type is a type expressing some congruence relation. In
-particular, it has a notion of composition of terms that is often used to derive
-proofs equationally.
-*)
-
-structure RHS = Generic_Data (
-  type T = (term * indexname) Termtab.table
-  val empty = Termtab.empty
-  val extend = I
-  val merge = Termtab.merge (Term.aconv o apply2 #1)
-)
-
-fun register_rhs t var =
-  let
-    val key = Term.head_of t
-    val idxname = #1 (dest_Var var)
-  in
-    RHS.map (Termtab.update (key, (t, idxname)))
-  end
-
-fun lookup_calc ctxt t =
-  Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t)
-
-
-(* Declaration *)
-
-local val Frees_to_Vars =
-  map_aterms (fn tm =>
-    case tm of
-      Free (name, T) => Var (("*!"^name, 0), T) (*FIXME: Hacky naming!*)
-    | _ => tm)
-in
-
-(*Declare the "right-hand side" of calculational types. Does not handle bound
-  variables, so no dependent RHS in declarations!*)
-val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>calc\<close>
-  "declare right hand side of calculational type"
-  (Parse.term -- (\<^keyword>\<open>rhs\<close> |-- Parse.term) >>
-    (fn (t_str, rhs_str) => fn lthy =>
-    let
-      val (t, rhs) = apply2 (Frees_to_Vars o Syntax.read_term lthy)
-        (t_str, rhs_str)
-    in lthy |>
-      Local_Theory.background_theory (
-        Context.theory_map (register_rhs t rhs))
-    end))
-
-end
-
-
-(* Ditto "''" setup *)
-
-fun last_rhs ctxt = map_aterms (fn t =>
-  case t of
-    Const (\<^const_name>\<open>rhs\<close>, _) =>
-      let
-        val this_name = Name_Space.full_name (Proof_Context.naming_of ctxt)
-          (Binding.name Auto_Bind.thisN)
-        val this = #thms (the (Proof_Context.lookup_fact ctxt this_name))
-          handle Option => []
-        val rhs =
-          (case map Thm.prop_of this of
-            [prop] =>
-              (let
-                val typ = Lib.type_of_typing (Logic.strip_assums_concl prop)
-                val (cong_pttrn, varname) = the (lookup_calc ctxt typ)
-                val unif_res = Pattern.unify (Context.Proof ctxt)
-                  (cong_pttrn, typ) Envir.init
-                val rhs = #2 (the
-                  (Vartab.lookup (Envir.term_env unif_res) varname))
-              in
-                rhs
-              end handle Option =>
-                error (".. can't match right-hand side of calculational type"))
-          | _ => Term.dummy)
-      in rhs end
-  | _ => t)
-
-val _ = Context.>>
-  (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt)))
-
-
-end
diff --git a/spartan/core/cases.ML b/spartan/core/cases.ML
deleted file mode 100644
index 560a9f1..0000000
--- a/spartan/core/cases.ML
+++ /dev/null
@@ -1,42 +0,0 @@
-(*  Title:      cases.ML
-    Author:     Joshua Chen
-
-Case reasoning.
-*)
-
-structure Case: sig
-
-val rules: Proof.context -> thm list
-val lookup_rule: Proof.context -> Termtab.key -> thm option
-val register_rule: thm -> Context.generic -> Context.generic
-
-end = struct
-
-(* Context data *)
-
-(*Stores elimination rules together with a list of the indexnames of the
-  variables each rule eliminates. Keyed by head of the type being eliminated.*)
-structure Rules = Generic_Data (
-  type T = thm Termtab.table
-  val empty = Termtab.empty
-  val extend = I
-  val merge = Termtab.merge Thm.eq_thm_prop
-)
-
-val rules = map #2 o Termtab.dest o Rules.get o Context.Proof
-fun lookup_rule ctxt = Termtab.lookup (Rules.get (Context.Proof ctxt))
-fun register_rule rl =
-  let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl))
-  in Rules.map (Termtab.update (hd, rl)) end
-
-
-(* [cases] attribute *)
-val _ = Theory.setup (
-  Attrib.setup \<^binding>\<open>cases\<close>
-    (Scan.succeed (Thm.declaration_attribute register_rule))
-    ""
-  #> Global_Theory.add_thms_dynamic (\<^binding>\<open>cases\<close>, rules o Context.proof_of)
-)
-
-
-end
diff --git a/spartan/core/comp.ML b/spartan/core/comp.ML
deleted file mode 100644
index 2e50753..0000000
--- a/spartan/core/comp.ML
+++ /dev/null
@@ -1,468 +0,0 @@
-(*  Title:      compute.ML
-    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
-    Modified:   Joshua Chen, University of Innsbruck
-
-This is a method for rewriting computational equalities that supports subterm
-selection based on patterns.
-
-This code has been slightly modified from the original at HOL/Library/compute.ML
-to incorporate automatic discharge of type-theoretic side conditions.
-
-Comment from the original code follows:
-
-The patterns accepted by compute are of the following form:
-  <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
-  <pattern> ::= (in <atom> | at <atom>) [<pattern>]
-  <args>    ::= [<pattern>] ("to" <term>) <thms>
-
-This syntax was clearly inspired by Gonthier's and Tassi's language of
-patterns but has diverged significantly during its development.
-
-We also allow introduction of identifiers for bound variables,
-which can then be used to match arbitrary subterms inside abstractions.
-*)
-
-infix 1 then_pconv;
-infix 0 else_pconv;
-
-signature COMPUTE =
-sig
-  type patconv = Proof.context -> Type.tyenv * (string * term) list -> cconv
-  val then_pconv: patconv * patconv -> patconv
-  val else_pconv: patconv * patconv -> patconv
-  val abs_pconv:  patconv -> string option * typ -> patconv (*XXX*)
-  val fun_pconv: patconv -> patconv
-  val arg_pconv: patconv -> patconv
-  val imp_pconv: patconv -> patconv
-  val params_pconv: patconv -> patconv
-  val forall_pconv: patconv -> string option * typ option -> patconv
-  val all_pconv: patconv
-  val for_pconv: patconv -> (string option * typ option) list -> patconv
-  val concl_pconv: patconv -> patconv
-  val asm_pconv: patconv -> patconv
-  val asms_pconv: patconv -> patconv
-  val judgment_pconv: patconv -> patconv
-  val in_pconv: patconv -> patconv
-  val match_pconv: patconv -> term * (string option * typ) list -> patconv
-  val comps_pconv: term option -> thm list -> patconv
-
-  datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
-
-  val mk_hole: int -> typ -> term
-
-  val compute_conv: Proof.context
-    -> (term * (string * typ) list, string * typ option) pattern list * term option
-    -> thm list
-    -> conv
-end
-
-structure Compute : COMPUTE =
-struct
-
-datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
-
-exception NO_TO_MATCH
-
-val holeN = Name.internal "_hole"
-
-fun prep_meta_eq ctxt = Simplifier.mksimps ctxt #> map Drule.zero_var_indexes
-
-
-(* holes *)
-
-fun mk_hole i T = Var ((holeN, i), T)
-
-fun is_hole (Var ((name, _), _)) = (name = holeN)
-  | is_hole _ = false
-
-fun is_hole_const (Const (\<^const_name>\<open>compute_hole\<close>, _)) = true
-  | is_hole_const _ = false
-
-val hole_syntax =
-  let
-    (* Modified variant of Term.replace_hole *)
-    fun replace_hole Ts (Const (\<^const_name>\<open>compute_hole\<close>, T)) i =
-          (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
-      | replace_hole Ts (Abs (x, T, t)) i =
-          let val (t', i') = replace_hole (T :: Ts) t i
-          in (Abs (x, T, t'), i') end
-      | replace_hole Ts (t $ u) i =
-          let
-            val (t', i') = replace_hole Ts t i
-            val (u', i'') = replace_hole Ts u i'
-          in (t' $ u', i'') end
-      | replace_hole _ a i = (a, i)
-    fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1)
-  in
-    Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes))
-    #> Proof_Context.set_mode Proof_Context.mode_pattern
-  end
-
-
-(* pattern conversions *)
-
-type patconv = Proof.context -> Type.tyenv * (string * term) list -> cterm -> thm
-
-fun (cv1 then_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv then_conv cv2 ctxt tytenv) ct
-
-fun (cv1 else_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv else_conv cv2 ctxt tytenv) ct
-
-fun raw_abs_pconv cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    Abs _ => CConv.abs_cconv (fn (x, ctxt') => cv x ctxt' tytenv) ctxt ct
-  | t => raise TERM ("raw_abs_pconv", [t])
-
-fun raw_fun_pconv cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct
-  | t => raise TERM ("raw_fun_pconv", [t])
-
-fun raw_arg_pconv cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    _ $ _ => CConv.arg_cconv (cv ctxt tytenv) ct
-  | t => raise TERM ("raw_arg_pconv", [t])
-
-fun abs_pconv cv (s,T) ctxt (tyenv, ts) ct =
-  let val u = Thm.term_of ct
-  in
-    case try (fastype_of #> dest_funT) u of
-      NONE => raise TERM ("abs_pconv: no function type", [u])
-    | SOME (U, _) =>
-        let
-          val tyenv' =
-            if T = dummyT then tyenv
-            else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
-          val eta_expand_cconv =
-            case u of
-              Abs _=> Thm.reflexive
-            | _ => CConv.rewr_cconv @{thm eta_expand}
-          fun add_ident NONE _ l = l
-            | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
-          val abs_cv = CConv.abs_cconv (fn (ct, ctxt) => cv ctxt (tyenv', add_ident s ct ts)) ctxt
-        in (eta_expand_cconv then_conv abs_cv) ct end
-        handle Pattern.MATCH => raise TYPE ("abs_pconv: types don't match", [T,U], [u])
-  end
-
-fun fun_pconv cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct
-  | Abs (_, T, _ $ Bound 0) => abs_pconv (fun_pconv cv) (NONE, T) ctxt tytenv ct
-  | t => raise TERM ("fun_pconv", [t])
-
-local
-
-fun arg_pconv_gen cv0 cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    _ $ _ => cv0 (cv ctxt tytenv) ct
-  | Abs (_, T, _ $ Bound 0) => abs_pconv (arg_pconv_gen cv0 cv) (NONE, T) ctxt tytenv ct
-  | t => raise TERM ("arg_pconv_gen", [t])
-
-in
-
-fun arg_pconv ctxt = arg_pconv_gen CConv.arg_cconv ctxt
-fun imp_pconv ctxt = arg_pconv_gen (CConv.concl_cconv 1) ctxt
-
-end
-
-(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
-fun params_pconv cv ctxt tytenv ct =
-  let val pconv =
-    case Thm.term_of ct of
-      Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs _ => (raw_arg_pconv o raw_abs_pconv) (fn _ => params_pconv cv)
-    | Const (\<^const_name>\<open>Pure.all\<close>, _) => raw_arg_pconv (params_pconv cv)
-    | _ => cv
-  in pconv ctxt tytenv ct end
-
-fun forall_pconv cv ident ctxt tytenv ct =
-  case Thm.term_of ct of
-    Const (\<^const_name>\<open>Pure.all\<close>, T) $ _ =>
-      let
-        val def_U = T |> dest_funT |> fst |> dest_funT |> fst
-        val ident' = apsnd (the_default (def_U)) ident
-      in arg_pconv (abs_pconv cv ident') ctxt tytenv ct end
-  | t => raise TERM ("forall_pconv", [t])
-
-fun all_pconv _ _ = Thm.reflexive
-
-fun for_pconv cv idents ctxt tytenv ct =
-  let
-    fun f rev_idents (Const (\<^const_name>\<open>Pure.all\<close>, _) $ t) =
-        let val (rev_idents', cv') = f rev_idents (case t of Abs (_,_,u) => u | _ => t)
-        in
-          case rev_idents' of
-            [] => ([], forall_pconv cv' (NONE, NONE))
-          | (x :: xs) => (xs, forall_pconv cv' x)
-        end
-      | f rev_idents _ = (rev_idents, cv)
-  in
-    case f (rev idents) (Thm.term_of ct) of
-      ([], cv') => cv' ctxt tytenv ct
-    | _ => raise CTERM ("for_pconv", [ct])
-  end
-
-fun concl_pconv cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _) $ _ => imp_pconv (concl_pconv cv) ctxt tytenv ct
-  | _ => cv ctxt tytenv ct
-
-fun asm_pconv cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _) $ _ => CConv.with_prems_cconv ~1 (cv ctxt tytenv) ct
-  | t => raise TERM ("asm_pconv", [t])
-
-fun asms_pconv cv ctxt tytenv ct =
-  case Thm.term_of ct of
-    (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _) $ _ =>
-      ((CConv.with_prems_cconv ~1 oo cv) else_pconv imp_pconv (asms_pconv cv)) ctxt tytenv ct
-  | t => raise TERM ("asms_pconv", [t])
-
-fun judgment_pconv cv ctxt tytenv ct =
-  if Object_Logic.is_judgment ctxt (Thm.term_of ct)
-  then arg_pconv cv ctxt tytenv ct
-  else cv ctxt tytenv ct
-
-fun in_pconv cv ctxt tytenv ct =
-  (cv else_pconv 
-   raw_fun_pconv (in_pconv cv) else_pconv
-   raw_arg_pconv (in_pconv cv) else_pconv
-   raw_abs_pconv (fn _  => in_pconv cv))
-  ctxt tytenv ct
-
-fun replace_idents idents t =
-  let
-    fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t
-      | subst _ t = t
-  in Term.map_aterms (subst idents) t end
-
-fun match_pconv cv (t,fixes) ctxt (tyenv, env_ts) ct =
-  let
-    val t' = replace_idents env_ts t
-    val thy = Proof_Context.theory_of ctxt
-    val u = Thm.term_of ct
-
-    fun descend_hole fixes (Abs (_, _, t)) =
-        (case descend_hole fixes t of
-          NONE => NONE
-        | SOME (fix :: fixes', pos) => SOME (fixes', abs_pconv pos fix)
-        | SOME ([], _) => raise Match (* less fixes than abstractions on path to hole *))
-      | descend_hole fixes (t as l $ r) =
-        let val (f, _) = strip_comb t
-        in
-          if is_hole f
-          then SOME (fixes, cv)
-          else
-            (case descend_hole fixes l of
-              SOME (fixes', pos) => SOME (fixes', fun_pconv pos)
-            | NONE =>
-              (case descend_hole fixes r of
-                SOME (fixes', pos) => SOME (fixes', arg_pconv pos)
-              | NONE => NONE))
-        end
-      | descend_hole fixes t =
-        if is_hole t then SOME (fixes, cv) else NONE
-
-    val to_hole = descend_hole (rev fixes) #> the_default ([], cv) #> snd
-  in
-    case try (Pattern.match thy (apply2 Logic.mk_term (t',u))) (tyenv, Vartab.empty) of
-      NONE => raise TERM ("match_pconv: Does not match pattern", [t, t',u])
-    | SOME (tyenv', _) => to_hole t ctxt (tyenv', env_ts) ct
-  end
-
-fun comps_pconv to thms ctxt (tyenv, env_ts) =
-  let
-    fun instantiate_normalize_env ctxt env thm =
-      let
-        val prop = Thm.prop_of thm
-        val norm_type = Envir.norm_type o Envir.type_env
-        val insts = Term.add_vars prop []
-          |> map (fn x as (s, T) =>
-              ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
-        val tyinsts = Term.add_tvars prop []
-          |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
-      in Drule.instantiate_normalize (tyinsts, insts) thm end
-    
-    fun unify_with_rhs context to env thm =
-      let
-        val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
-        val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
-          handle Pattern.Unif => raise NO_TO_MATCH
-      in env' end
-    
-    fun inst_thm_to _ (NONE, _) thm = thm
-      | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
-          instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
-    
-    fun inst_thm ctxt idents (to, tyenv) thm =
-      let
-        (* Replace any identifiers with their corresponding bound variables. *)
-        val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
-        val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
-        val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
-        val thm' = Thm.incr_indexes (maxidx + 1) thm
-      in SOME (inst_thm_to ctxt (Option.map (replace_idents idents) to, env) thm') end
-      handle NO_TO_MATCH => NONE
-    
-  in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end
-
-fun compute_conv ctxt (pattern, to) thms ct =
-  let
-    fun apply_pat At = judgment_pconv
-      | apply_pat In = in_pconv
-      | apply_pat Asm = params_pconv o asms_pconv
-      | apply_pat Concl = params_pconv o concl_pconv
-      | apply_pat (For idents) = (fn cv => for_pconv cv (map (apfst SOME) idents))
-      | apply_pat (Term x) = (fn cv => match_pconv cv (apsnd (map (apfst SOME)) x))
-
-    val cv = fold_rev apply_pat pattern
-
-    fun distinct_prems th =
-      case Seq.pull (distinct_subgoals_tac th) of
-        NONE => th
-      | SOME (th', _) => th'
-
-    val compute = comps_pconv to (maps (prep_meta_eq ctxt) thms)
-  in cv compute ctxt (Vartab.empty, []) ct |> distinct_prems end
-
-fun compute_export_tac ctxt (pat, pat_ctxt) thms =
-  let
-    val export = case pat_ctxt of
-        NONE => I
-      | SOME inner => singleton (Proof_Context.export inner ctxt)
-  in CCONVERSION (export o compute_conv ctxt pat thms) end
-
-val _ =
-  Theory.setup
-  let
-    fun mk_fix s = (Binding.name s, NONE, NoSyn)
-
-    val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
-      let
-        val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
-        val atom =  (Args.$$$ "asm" >> K Asm) ||
-          (Args.$$$ "concl" >> K Concl) ||
-          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) ||
-          (Parse.term >> Term)
-        val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
-
-        fun append_default [] = [Concl, In]
-          | append_default (ps as Term _ :: _) = Concl :: In :: ps
-          | append_default [For x, In] = [For x, Concl, In]
-          | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
-          | append_default ps = ps
-
-      in Scan.repeats sep_atom >> (rev #> append_default) end
-
-    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
-      let
-        val (r, toks') = scan toks
-        val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
-      in (r', (context', toks' : Token.T list)) end
-
-    fun read_fixes fixes ctxt =
-      let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
-      in Proof_Context.add_fixes (map read_typ fixes) ctxt end
-
-    fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
-      let
-        fun add_constrs ctxt n (Abs (x, T, t)) =
-            let
-              val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
-            in
-              (case add_constrs ctxt' (n+1) t of
-                NONE => NONE
-              | SOME ((ctxt'', n', xs), t') =>
-                  let
-                    val U = Type_Infer.mk_param n []
-                    val u = Type.constraint (U --> dummyT) (Abs (x, T, t'))
-                  in SOME ((ctxt'', n', (x', U) :: xs), u) end)
-            end
-          | add_constrs ctxt n (l $ r) =
-            (case add_constrs ctxt n l of
-              SOME (c, l') => SOME (c, l' $ r)
-            | NONE =>
-              (case add_constrs ctxt n r of
-                SOME (c, r') => SOME (c, l $ r')
-              | NONE => NONE))
-          | add_constrs ctxt n t =
-            if is_hole_const t then SOME ((ctxt, n, []), t) else NONE
-
-        fun prep (Term s) (n, ctxt) =
-            let
-              val t = Syntax.parse_term ctxt s
-              val ((ctxt', n', bs), t') =
-                the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t)
-            in (Term (t', bs), (n', ctxt')) end
-          | prep (For ss) (n, ctxt) =
-            let val (ns, ctxt') = read_fixes ss ctxt
-            in (For ns, (n, ctxt')) end
-          | prep At (n,ctxt) = (At, (n, ctxt))
-          | prep In (n,ctxt) = (In, (n, ctxt))
-          | prep Concl (n,ctxt) = (Concl, (n, ctxt))
-          | prep Asm (n,ctxt) = (Asm, (n, ctxt))
-
-        val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt)
-
-      in (xs, ctxt') end
-
-    fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) =
-      let
-
-        fun check_terms ctxt ps to =
-          let
-            fun safe_chop (0: int) xs = ([], xs)
-              | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x
-              | safe_chop _ _ = raise Match
-
-            fun reinsert_pat _ (Term (_, cs)) (t :: ts) =
-                let val (cs', ts') = safe_chop (length cs) ts
-                in (Term (t, map dest_Free cs'), ts') end
-              | reinsert_pat _ (Term _) [] = raise Match
-              | reinsert_pat ctxt (For ss) ts =
-                let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss
-                in (For fixes, ts) end
-              | reinsert_pat _ At ts = (At, ts)
-              | reinsert_pat _ In ts = (In, ts)
-              | reinsert_pat _ Concl ts = (Concl, ts)
-              | reinsert_pat _ Asm ts = (Asm, ts)
-
-            fun free_constr (s,T) = Type.constraint T (Free (s, dummyT))
-            fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
-              | mk_free_constrs _ = []
-
-            val ts = maps mk_free_constrs ps @ the_list to
-              |> Syntax.check_terms (hole_syntax ctxt)
-            val ctxt' = fold Variable.declare_term ts ctxt
-            val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts
-              ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs))
-            val _ = case ts' of (_ :: _) => raise Match | [] => ()
-          in ((ps', to'), ctxt') end
-
-        val (pats, ctxt') = prep_pats ctxt raw_pats
-
-        val ths = Attrib.eval_thms ctxt' raw_ths
-        val to = Option.map (Syntax.parse_term ctxt') raw_to
-
-        val ((pats', to'), ctxt'') = check_terms ctxt' pats to
-
-      in ((pats', ths, (to', ctxt)), ctxt'') end
-
-    val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
-
-    val subst_parser =
-      let val scan = raw_pattern -- to_parser -- Parse.thms1
-      in context_lift scan prep_args end
-
-    fun compute_export_ctac inputs inthms =
-      CONTEXT_TACTIC' (fn ctxt => compute_export_tac ctxt inputs inthms)
-  in
-    Method.setup \<^binding>\<open>cmp\<close> (subst_parser >>
-      (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD'
-        (compute_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
-      "single-step rewriting, allowing subterm selection via patterns" #>
-    Method.setup \<^binding>\<open>comp\<close> (subst_parser >>
-      (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD (
-        CHEADGOAL o SIDE_CONDS 0
-          (compute_export_ctac ((pattern, to), SOME pat_ctxt) inthms)))))
-      "single-step rewriting with auto-typechecking"
-  end
-end
diff --git a/spartan/core/context_facts.ML b/spartan/core/context_facts.ML
deleted file mode 100644
index 5aa7c70..0000000
--- a/spartan/core/context_facts.ML
+++ /dev/null
@@ -1,101 +0,0 @@
-structure Context_Facts: sig
-
-val Known: Proof.context -> thm Item_Net.T
-val known: Proof.context -> thm list
-val known_of: Proof.context -> term -> thm list
-val register_known: thm -> Context.generic -> Context.generic
-val register_knowns: thm list -> Context.generic -> Context.generic
-
-val Cond: Proof.context -> thm Item_Net.T
-val cond: Proof.context -> thm list
-val cond_of: Proof.context -> term -> thm list
-val register_cond: thm -> Context.generic -> Context.generic
-val register_conds: thm list -> Context.generic -> Context.generic
-
-val Eq: Proof.context -> thm Item_Net.T
-val eq: Proof.context -> thm list
-val eq_of: Proof.context -> term -> thm list
-val register_eq: thm -> Context.generic -> Context.generic
-val register_eqs: thm list -> Context.generic -> Context.generic
-
-val register_facts: thm list -> Proof.context -> Proof.context
-
-end = struct
-
-(* Known types *)
-
-structure Known = Generic_Data (
-  type T = thm Item_Net.T
-  val empty = Item_Net.init Thm.eq_thm
-    (single o Lib.term_of_typing o Thm.prop_of)
-  val extend = I
-  val merge = Item_Net.merge
-)
-
-val Known = Known.get o Context.Proof
-val known = Item_Net.content o Known
-fun known_of ctxt tm = Item_Net.retrieve (Known ctxt) tm
-
-fun register_known typing =
-  if Lib.is_typing (Thm.prop_of typing) then Known.map (Item_Net.update typing)
-  else error "Not a type judgment"
-
-fun register_knowns typings = foldr1 (op o) (map register_known typings)
-
-
-(* Conditional type rules *)
-
-(*Two important cases: 1. general type inference rules and 2. type family
-  judgments*)
-
-structure Cond = Generic_Data (
-  type T = thm Item_Net.T
-  val empty = Item_Net.init Thm.eq_thm
-    (single o Lib.term_of_typing o Thm.concl_of)
-  val extend = I
-  val merge = Item_Net.merge
-)
-
-val Cond = Cond.get o Context.Proof
-val cond = Item_Net.content o Cond
-fun cond_of ctxt tm = Item_Net.retrieve (Cond ctxt) tm
-
-fun register_cond rule =
-  if Lib.is_typing (Thm.concl_of rule) then Cond.map (Item_Net.update rule)
-  else error "Not a conditional type judgment"
-
-fun register_conds rules = foldr1 (op o) (map register_cond rules)
-
-
-(* Equality statements *)
-
-structure Eq = Generic_Data (
-  type T = thm Item_Net.T
-  val empty = Item_Net.init Thm.eq_thm
-    (single o (#1 o Lib.dest_eq) o Thm.concl_of)
-  val extend = I
-  val merge = Item_Net.merge
-)
-
-val Eq = Eq.get o Context.Proof
-val eq = Item_Net.content o Eq
-fun eq_of ctxt tm = Item_Net.retrieve (Eq ctxt) tm
-
-fun register_eq rule =
-  if Lib.is_eq (Thm.concl_of rule) then Eq.map (Item_Net.update rule)
-  else error "Not a definitional equality judgment"
-
-fun register_eqs rules = foldr1 (op o) (map register_eq rules)
-
-
-(* Context assumptions *)
-
-fun register_facts ths =
-  let
-    val (facts, conds, eqs) = Lib.partition_judgments ths
-    val f = register_knowns facts handle Empty => I
-    val c = register_conds conds handle Empty => I
-    val e = register_eqs eqs handle Empty => I
-  in Context.proof_map (e o c o f) end
-
-end
diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML
deleted file mode 100644
index d0fed61..0000000
--- a/spartan/core/context_tactical.ML
+++ /dev/null
@@ -1,256 +0,0 @@
-(*  Title:      context_tactical.ML
-    Author:     Joshua Chen
-
-More context tactics, and context tactic combinators.
-
-Contains code modified from
-  ~~/Pure/search.ML
-  ~~/Pure/tactical.ML
-*)
-
-infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD
-infix 0 CORELSE CAPPEND CORELSE' CAPPEND'
-
-structure Context_Tactical:
-sig
-
-type context_tactic' = int -> context_tactic
-val CONTEXT_TACTIC': (Proof.context -> int -> tactic) -> context_tactic'
-val all_ctac: context_tactic
-val no_ctac: context_tactic
-val print_ctac: (Proof.context -> string) -> context_tactic
-val CTHEN: context_tactic * context_tactic -> context_tactic
-val CORELSE: context_tactic * context_tactic -> context_tactic
-val CAPPEND: context_tactic * context_tactic -> context_tactic
-val CTHEN': context_tactic' * context_tactic' -> context_tactic'
-val CORELSE': context_tactic' * context_tactic' -> context_tactic'
-val CAPPEND': context_tactic' * context_tactic' -> context_tactic'
-val CTRY: context_tactic -> context_tactic
-val CREPEAT: context_tactic -> context_tactic
-val CREPEAT1: context_tactic -> context_tactic
-val CREPEAT_N: int -> context_tactic -> context_tactic
-val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic
-val CCHANGED: context_tactic -> context_tactic
-val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic'
-val CREPEAT_IN_RANGE: int -> int -> context_tactic' -> context_tactic
-val CREPEAT_ALL_NEW: context_tactic' -> context_tactic'
-val CTHEN_ALL_NEW_FWD: context_tactic' * context_tactic' -> context_tactic'
-val CREPEAT_ALL_NEW_FWD: context_tactic' -> context_tactic'
-val CHEADGOAL: context_tactic' -> context_tactic
-val CALLGOALS: context_tactic' -> context_tactic
-val CSOMEGOAL: context_tactic' -> context_tactic
-val CRANGE: context_tactic' list -> context_tactic'
-val CFIRST: context_tactic list -> context_tactic
-val CFIRST': context_tactic' list -> context_tactic'
-val CTHEN_BEST_FIRST: context_tactic -> (context_state -> bool) ->
-  (context_state -> int) -> context_tactic -> context_tactic
-val CBEST_FIRST: (context_state -> bool) -> (context_state -> int) ->
-  context_tactic -> context_tactic
-val CTHEN_ASTAR: context_tactic -> (context_state -> bool) ->
-  (int -> context_state -> int) -> context_tactic -> context_tactic
-val CASTAR: (context_state -> bool) -> (int -> context_state -> int) ->
-  context_tactic -> context_tactic
-
-end = struct
-
-type context_tactic' = int -> context_tactic
-
-fun CONTEXT_TACTIC' tac i (ctxt, st) = TACTIC_CONTEXT ctxt ((tac ctxt i) st)
-
-val all_ctac = Seq.make_results o Seq.single
-val no_ctac = K Seq.empty
-fun print_ctac f (ctxt, st) = CONTEXT_TACTIC (print_tac ctxt (f ctxt)) (ctxt, st)
-
-fun (ctac1 CTHEN ctac2) cst =  Seq.maps_results ctac2 (ctac1 cst)
-
-fun (ctac1 CORELSE ctac2) cst =
-  (case Seq.pull (ctac1 cst) of
-    NONE => ctac2 cst
-  | some => Seq.make (fn () => some))
-
-fun (ctac1 CAPPEND ctac2) cst =
-  Seq.append (ctac1 cst) (Seq.make (fn () => Seq.pull (ctac2 cst)))
-
-fun (ctac1 CTHEN' ctac2) x = ctac1 x CTHEN ctac2 x
-fun (ctac1 CORELSE' ctac2) x = ctac1 x CORELSE ctac2 x
-fun (ctac1 CAPPEND' ctac2) x = ctac1 x CAPPEND ctac2 x
-
-fun CTRY ctac = ctac CORELSE all_ctac
-
-fun CREPEAT ctac =
-  let
-    fun rep qs cst =
-      (case Seq.pull (Seq.filter_results (ctac cst)) of
-        NONE => SOME (cst, Seq.make (fn () => repq qs))
-      | SOME (cst', q) => rep (q :: qs) cst')
-    and repq [] = NONE
-      | repq (q :: qs) =
-          (case Seq.pull q of
-            NONE => repq qs
-          | SOME (cst, q) => rep (q :: qs) cst);
-  in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end
-
-fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
-
-fun CREPEAT_N 0 _ = no_ctac
-  | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac
-
-fun CFILTER pred ctac cst =
-  ctac cst
-  |> Seq.filter_results
-  |> Seq.filter pred
-  |> Seq.make_results
-
-(*Only accept next states where the subgoals have changed*)
-fun CCHANGED ctac (cst as (_, st)) =
-  CFILTER (fn (_, st') => not (Thm.eq_thm (st, st'))) ctac cst
-
-local
-  fun op THEN (f, g) x = Seq.maps_results g (f x)
-
-  fun INTERVAL f i j x =
-    if i > j then Seq.make_results (Seq.single x)
-    else op THEN (f j, INTERVAL f i (j - 1)) x
-
-  (*By Peter Lammich: apply tactic to subgoals in interval in a forward manner,
-    skipping over emerging subgoals*)
-  fun INTERVAL_FWD ctac l u (cst as (_, st)) = cst |>
-    (if l > u then all_ctac
-    else (ctac l CTHEN (fn cst' as (_, st') =>
-      let val ofs = Thm.nprems_of st' - Thm.nprems_of st in
-        if ofs < ~1
-        then raise THM (
-          "INTERVAL_FWD: tactic solved more than one goal", ~1, [st, st'])
-        else INTERVAL_FWD ctac (l + 1 + ofs) (u + ofs) cst'
-      end)))
-in
-
-fun (ctac1 CTHEN_ALL_NEW ctac2) i (cst as (_, st)) =
-  cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
-    INTERVAL ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst'))
-
-(*By Peter Lammich: apply ctac2 to all subgoals emerging from ctac1, in forward
-  manner*)
-fun (ctac1 CTHEN_ALL_NEW_FWD ctac2) i (cst as (_, st)) =
-  cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
-    INTERVAL_FWD ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst'))
-
-(*Repeatedly apply ctac to the i-th until the k-th-from-last subgoals
-  (i.e. leave the last k subgoals alone), until no more changes appear in the
-  goal state.*)
-fun CREPEAT_IN_RANGE i k ctac =
-  let fun interval_ctac (cst as (_, st)) =
-    INTERVAL_FWD ctac i (Thm.nprems_of st - k) cst
-  in CREPEAT (CCHANGED interval_ctac) end
-
-end
-
-fun CREPEAT_ALL_NEW ctac =
-  ctac CTHEN_ALL_NEW (CTRY o (fn i => CREPEAT_ALL_NEW ctac i))
-
-fun CREPEAT_ALL_NEW_FWD ctac =
-  ctac CTHEN_ALL_NEW_FWD (CTRY o (fn i => CREPEAT_ALL_NEW_FWD ctac i))
-
-fun CHEADGOAL ctac = ctac 1
-
-fun CALLGOALS ctac (cst as (_, st)) =
-  let
-    fun doall 0 = all_ctac
-      | doall n = ctac n CTHEN doall (n - 1);
-  in doall (Thm.nprems_of st) cst end
-
-fun CSOMEGOAL ctac (cst as (_, st)) =
-  let
-    fun find 0 = no_ctac
-      | find n = ctac n CORELSE find (n - 1);
-  in find (Thm.nprems_of st) cst end
-
-fun CRANGE [] _ = all_ctac
-  | CRANGE (ctac :: ctacs) i = CRANGE ctacs (i + 1) CTHEN ctac i
-
-fun CFIRST ctacs = fold_rev (curry op CORELSE) ctacs no_ctac
-
-(*FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i*)
-fun CFIRST' ctacs = fold_rev (curry op CORELSE') ctacs (K no_ctac)
-
-
-(** Search tacticals **)
-
-(* Best-first search *)
-
-structure Thm_Heap = Heap (
-  type elem = int * thm;
-  val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of)
-)
-
-structure Context_State_Heap = Heap (
-  type elem = int * context_state;
-  val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 (Thm.prop_of o #2))
-)
-
-fun some_of_list [] = NONE
-  | some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l))
-
-(*Check for and delete duplicate proof states*)
-fun delete_all_min (cst as (_, st)) heap =
-  if Context_State_Heap.is_empty heap then heap
-  else if Thm.eq_thm (st, #2 (#2 (Context_State_Heap.min heap)))
-  then delete_all_min cst (Context_State_Heap.delete_min heap)
-  else heap
-
-(*Best-first search for a state that satisfies satp (incl initial state)
-  Function sizef estimates size of problem remaining (smaller means better).
-  tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
-fun CTHEN_BEST_FIRST ctac0 satp sizef ctac =
-  let
-    fun pairsize cst = (sizef cst, cst);
-    fun bfs (news, nst_heap) =
-      (case List.partition satp news of
-        ([], nonsats) => next (fold_rev Context_State_Heap.insert (map pairsize nonsats) nst_heap)
-      | (sats, _)  => some_of_list sats)
-    and next nst_heap =
-      if Context_State_Heap.is_empty nst_heap then NONE
-      else
-        let
-          val (n, cst) = Context_State_Heap.min nst_heap;
-        in
-          bfs (Seq.list_of (Seq.filter_results (ctac cst)), delete_all_min cst (Context_State_Heap.delete_min nst_heap))
-        end;
-    fun btac cst = bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), Context_State_Heap.empty)
-  in fn cst => Seq.make_results (Seq.make (fn () => btac cst)) end
-
-(*Ordinary best-first search, with no initial tactic*)
-val CBEST_FIRST = CTHEN_BEST_FIRST all_ctac
-
-
-(* A*-like search *)
-
-(*Insertion into priority queue of states, marked with level*)
-fun insert_with_level (lnth: int * int * context_state) [] = [lnth]
-  | insert_with_level (l, m, cst) ((l', n, cst') :: csts) =
-      if  n < m then (l', n, cst') :: insert_with_level (l, m, cst) csts
-      else if n = m andalso Thm.eq_thm (#2 cst, #2 cst') then (l', n, cst') :: csts
-      else (l, m, cst) :: (l', n, cst') :: csts;
-
-fun CTHEN_ASTAR ctac0 satp costf ctac =
-  let
-    fun bfs (news, nst, level) =
-      let fun cost cst = (level, costf level cst, cst) in
-        (case List.partition satp news of
-          ([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nst)
-        | (sats, _) => some_of_list sats)
-      end
-    and next [] = NONE
-      | next ((level, n, cst) :: nst) =
-          bfs (Seq.list_of (Seq.filter_results (ctac cst)), nst, level + 1)
-  in fn cst => Seq.make_results
-    (Seq.make (fn () => bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), [], 0)))
-  end
-
-(*Ordinary ASTAR, with no initial tactic*)
-val CASTAR = CTHEN_ASTAR all_ctac;
-
-
-end
-
-open Context_Tactical
diff --git a/spartan/core/elaborated_statement.ML b/spartan/core/elaborated_statement.ML
deleted file mode 100644
index 33f88cf..0000000
--- a/spartan/core/elaborated_statement.ML
+++ /dev/null
@@ -1,470 +0,0 @@
-(*  Title:      elaborated_statement.ML
-    Author:     Joshua Chen
-
-Term elaboration for goal statements and proof commands.
-
-Contains code from parts of
-  ~~/Pure/Isar/element.ML and
-  ~~/Pure/Isar/expression.ML
-in both verbatim and modified forms.
-*)
-
-structure Elaborated_Statement: sig
-
-val read_goal_statement:
-  (string, string, Facts.ref) Element.ctxt list ->
-  (string, string) Element.stmt ->
-  Proof.context ->
-  (Attrib.binding * (term * term list) list) list * Proof.context
-
-end = struct
-
-
-(* Elaborated goal statements *)
-
-local
-
-fun mk_type T = (Logic.mk_type T, [])
-fun mk_term t = (t, [])
-fun mk_propp (p, pats) = (Type.constraint propT p, pats)
-
-fun dest_type (T, []) = Logic.dest_type T
-fun dest_term (t, []) = t
-fun dest_propp (p, pats) = (p, pats)
-
-fun extract_inst (_, (_, ts)) = map mk_term ts
-fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs))
-
-fun extract_eqns es = map (mk_term o snd) es
-fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs
-
-fun extract_elem (Element.Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes
-  | extract_elem (Element.Constrains csts) = map (#2 #> single #> map mk_type) csts
-  | extract_elem (Element.Assumes asms) = map (#2 #> map mk_propp) asms
-  | extract_elem (Element.Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
-  | extract_elem (Element.Notes _) = []
-  | extract_elem (Element.Lazy_Notes _) = []
-
-fun restore_elem (Element.Fixes fixes, css) =
-      (fixes ~~ css) |> map (fn ((x, _, mx), cs) =>
-        (x, cs |> map dest_type |> try hd, mx)) |> Element.Fixes
-  | restore_elem (Element.Constrains csts, css) =
-      (csts ~~ css) |> map (fn ((x, _), cs) =>
-        (x, cs |> map dest_type |> hd)) |> Element.Constrains
-  | restore_elem (Element.Assumes asms, css) =
-      (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Element.Assumes
-  | restore_elem (Element.Defines defs, css) =
-      (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Element.Defines
-  | restore_elem (elem as Element.Notes _, _) = elem
-  | restore_elem (elem as Element.Lazy_Notes _, _) = elem
-
-fun prep (_, pats) (ctxt, t :: ts) =
-  let val ctxt' = Proof_Context.augment t ctxt
-  in
-    ((t, Syntax.check_props
-        (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
-      (ctxt', ts))
-  end
-
-fun check cs ctxt =
-  let
-    val (cs', (ctxt', _)) = fold_map prep cs
-      (ctxt, Syntax.check_terms
-        (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs))
-  in (cs', ctxt') end
-
-fun inst_morphism params ((prfx, mandatory), insts') ctxt =
-  let
-    (*parameters*)
-    val parm_types = map #2 params;
-    val type_parms = fold Term.add_tfreesT parm_types [];
-
-    (*type inference*)
-    val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
-    val type_parms' = fold Term.add_tvarsT parm_types' [];
-    val checked =
-      (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts')
-      |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt)
-    val (type_parms'', insts'') = chop (length type_parms') checked;
-
-    (*context*)
-    val ctxt' = fold Proof_Context.augment checked ctxt;
-    val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt';
-    val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt';
-
-    (*instantiation*)
-    val instT =
-      (type_parms ~~ map Logic.dest_type type_parms'')
-      |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
-    val cert_inst =
-      ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
-      |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
-  in
-    (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
-      Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
-  end;
-
-fun abs_def ctxt =
-  Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of;
-
-fun declare_elem prep_var (Element.Fixes fixes) ctxt =
-      let val (vars, _) = fold_map prep_var fixes ctxt
-      in ctxt |> Proof_Context.add_fixes vars |> snd end
-  | declare_elem prep_var (Element.Constrains csts) ctxt =
-      ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd
-  | declare_elem _ (Element.Assumes _) ctxt = ctxt
-  | declare_elem _ (Element.Defines _) ctxt = ctxt
-  | declare_elem _ (Element.Notes _) ctxt = ctxt
-  | declare_elem _ (Element.Lazy_Notes _) ctxt = ctxt;
-
-fun parameters_of thy strict (expr, fixed) =
-  let
-    val ctxt = Proof_Context.init_global thy;
-
-    fun reject_dups message xs =
-      (case duplicates (op =) xs of
-        [] => ()
-      | dups => error (message ^ commas dups));
-
-    fun parm_eq ((p1, mx1), (p2, mx2)) =
-      p1 = p2 andalso
-        (Mixfix.equal (mx1, mx2) orelse
-          error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^
-            Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2]));
-
-    fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
-    fun params_inst (loc, (prfx, (Expression.Positional insts, eqns))) =
-          let
-            val ps = params_loc loc;
-            val d = length ps - length insts;
-            val insts' =
-              if d < 0 then
-                error ("More arguments than parameters in instantiation of locale " ^
-                  quote (Locale.markup_name ctxt loc))
-              else insts @ replicate d NONE;
-            val ps' = (ps ~~ insts') |>
-              map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
-          in (ps', (loc, (prfx, (Expression.Positional insts', eqns)))) end
-      | params_inst (loc, (prfx, (Expression.Named insts, eqns))) =
-          let
-            val _ =
-              reject_dups "Duplicate instantiation of the following parameter(s): "
-                (map fst insts);
-            val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
-              if AList.defined (op =) ps p then AList.delete (op =) p ps
-              else error (quote p ^ " not a parameter of instantiated expression"));
-          in (ps', (loc, (prfx, (Expression.Named insts, eqns)))) end;
-    fun params_expr is =
-      let
-        val (is', ps') = fold_map (fn i => fn ps =>
-          let
-            val (ps', i') = params_inst i;
-            val ps'' = distinct parm_eq (ps @ ps');
-          in (i', ps'') end) is []
-      in (ps', is') end;
-
-    val (implicit, expr') = params_expr expr;
-
-    val implicit' = map #1 implicit;
-    val fixed' = map (Variable.check_name o #1) fixed;
-    val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
-    val implicit'' =
-      if strict then []
-      else
-        let
-          val _ =
-            reject_dups
-              "Parameter(s) declared simultaneously in expression and for clause: "
-              (implicit' @ fixed');
-        in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
-  in (expr', implicit'' @ fixed) end;
-
-fun parse_elem prep_typ prep_term ctxt =
-  Element.map_ctxt
-   {binding = I,
-    typ = prep_typ ctxt,
-    term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt),
-    pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt),
-    fact = I,
-    attrib = I};
-
-fun prepare_stmt prep_prop prep_obtains ctxt stmt =
-  (case stmt of
-    Element.Shows raw_shows =>
-      raw_shows |> (map o apsnd o map) (fn (t, ps) =>
-        (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
-          map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps))
-  | Element.Obtains raw_obtains =>
-      let
-        val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt;
-        val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
-      in map (fn (b, t) => ((b, []), [(t, [])])) obtains end);
-
-fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
-  let val x = Binding.name_of binding
-  in (binding, AList.lookup (op =) parms x, mx) end)
-
-fun finish_inst ctxt (loc, (prfx, inst)) =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt;
-  in (loc, morph) end
-
-fun closeup _ _ false elem = elem
-  | closeup (outer_ctxt, ctxt) parms true elem =
-      let
-        (*FIXME consider closing in syntactic phase -- before type checking*)
-        fun close_frees t =
-          let
-            val rev_frees =
-              Term.fold_aterms (fn Free (x, T) =>
-                if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I
-                else insert (op =) (x, T) | _ => I) t [];
-          in fold (Logic.all o Free) rev_frees t end;
-
-        fun no_binds [] = []
-          | no_binds _ = error "Illegal term bindings in context element";
-      in
-        (case elem of
-          Element.Assumes asms => Element.Assumes (asms |> map (fn (a, propps) =>
-            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
-        | Element.Defines defs => Element.Defines (defs |> map (fn ((name, atts), (t, ps)) =>
-            let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t)
-            in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
-        | e => e)
-      end
-
-fun finish_elem _ parms _ (Element.Fixes fixes) = Element.Fixes (finish_fixes parms fixes)
-  | finish_elem _ _ _ (Element.Constrains _) = Element.Constrains []
-  | finish_elem ctxts parms do_close (Element.Assumes asms) = closeup ctxts parms do_close (Element.Assumes asms)
-  | finish_elem ctxts parms do_close (Element.Defines defs) = closeup ctxts parms do_close (Element.Defines defs)
-  | finish_elem _ _ _ (elem as Element.Notes _) = elem
-  | finish_elem _ _ _ (elem as Element.Lazy_Notes _) = elem
-
-fun check_autofix insts eqnss elems concl ctxt =
-  let
-    val inst_cs = map extract_inst insts;
-    val eqns_cs = map extract_eqns eqnss;
-    val elem_css = map extract_elem elems;
-    val concl_cs = (map o map) mk_propp (map snd concl);
-    (*Type inference*)
-    val (inst_cs' :: eqns_cs' :: css', ctxt') =
-      (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt;
-    val (elem_css', [concl_cs']) = chop (length elem_css) css';
-  in
-    ((map restore_inst (insts ~~ inst_cs'),
-      map restore_eqns (eqnss ~~ eqns_cs'),
-      map restore_elem (elems ~~ elem_css'),
-      map fst concl ~~ concl_cs'), ctxt')
-  end
-
-fun prep_full_context_statement
-  parse_typ parse_prop
-  prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr
-  {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt
-  ctxt1
-  =
-  let
-    val thy = Proof_Context.theory_of ctxt1
-    val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import)
-    fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
-      let
-        val params = map #1 (Locale.params_of thy loc)
-        val inst' = prep_inst ctxt (map #1 params) inst
-        val parm_types' =
-          params |> map (#2 #> Logic.varifyT_global #>
-              Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
-              Type_Infer.paramify_vars)
-        val inst'' = map2 Type.constraint parm_types' inst'
-        val insts' = insts @ [(loc, (prfx, inst''))]
-        val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt
-        val inst''' = insts'' |> List.last |> snd |> snd
-        val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt
-        val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2
-          handle ERROR msg => if null eqns then error msg else
-            (Locale.tracing ctxt1
-             (msg ^ "\nFalling back to reading rewrites clause before activation.");
-             ctxt2)
-        val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns
-        val eqns' = (prep_eqns ctxt' o map snd) eqns
-        val eqnss' = [attrss ~~ eqns']
-        val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt'
-        val rewrite_morph = eqns'
-          |> map (abs_def ctxt')
-          |> Variable.export_terms ctxt' ctxt
-          |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
-          |> the_default Morphism.identity
-       val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt
-       val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns']
-      in (i + 1, insts', eqnss', ctxt'') end
-
-    fun prep_elem raw_elem ctxt =
-      let
-        val ctxt' = ctxt
-          |> Context_Position.set_visible false
-          |> declare_elem prep_var_elem raw_elem
-          |> Context_Position.restore_visible ctxt
-        val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem
-      in (elems', ctxt') end
-
-    val fors = fold_map prep_var_inst fixed ctxt1 |> fst
-    val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd
-    val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2)
-
-    fun prep_stmt elems ctxt =
-      check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt
-
-    val _ =
-      if fixed_frees then ()
-      else
-        (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of
-          [] => ()
-        | frees => error ("Illegal free variables in expression: " ^
-            commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))))
-
-    val ((insts, _, elems', concl), ctxt4) = ctxt3
-      |> init_body
-      |> fold_map prep_elem raw_elems
-      |-> prep_stmt
-
-    (*parameters from expression and elements*)
-    val xs = maps (fn Element.Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
-      (Element.Fixes fors :: elems')
-    val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4
-    val fors' = finish_fixes parms fors
-    val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors'
-    val deps = map (finish_inst ctxt5) insts
-    val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems'
-  in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end
-
-fun prep_inst prep_term ctxt parms (Expression.Positional insts) =
-      (insts ~~ parms) |> map
-        (fn (NONE, p) => Free (p, dummyT)
-          | (SOME t, _) => prep_term ctxt t)
-  | prep_inst prep_term ctxt parms (Expression.Named insts) =
-      parms |> map (fn p =>
-        (case AList.lookup (op =) insts p of
-          SOME t => prep_term ctxt t |
-          NONE => Free (p, dummyT)))
-fun parse_inst x = prep_inst Syntax.parse_term x
-fun check_expr thy instances = map (apfst (Locale.check thy)) instances
-
-val read_full_context_statement = prep_full_context_statement
-  Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
-  Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src
-  Proof_Context.read_var check_expr
-
-fun filter_assumes ((x as Element.Assumes _) :: xs) = x :: filter_assumes xs
-  | filter_assumes (_ :: xs) = filter_assumes xs
-  | filter_assumes [] = []
-
-fun prep_statement prep activate raw_elems raw_stmt ctxt =
-  let
-    val ((_, _, _, elems, concl), _) =
-      prep {strict = true, do_close = false, fixed_frees = true}
-        ([], []) I raw_elems raw_stmt ctxt
-
-    val (elems', ctxt') = ctxt
-      |> Proof_Context.set_stmt true
-      |> fold_map activate elems
-      |> apsnd (Proof_Context.restore_stmt ctxt)
-
-    val assumes = filter_assumes elems'
-    val assms = flat (flat (map
-      (fn (Element.Assumes asms) =>
-        map (fn (_, facts) => map (Thm.cterm_of ctxt' o #1) facts) asms)
-      assumes))
-    val concl' = Elab.elaborate ctxt' assms concl handle error => concl
-  in (concl', ctxt') end
-
-fun activate_i elem ctxt =
-  let
-    val elem' =
-      (case (Element.map_ctxt_attrib o map) Token.init_assignable elem of
-        Element.Defines defs =>
-          Element.Defines (defs |> map (fn ((a, atts), (t, ps)) =>
-            ((Thm.def_binding_optional
-              (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts),
-              (t, ps))))
-      | Element.Assumes assms => Element.Assumes (Elab.elaborate ctxt [] assms)
-      | e => e);
-    val ctxt' = Context.proof_map (Element.init elem') ctxt;
-  in ((Element.map_ctxt_attrib o map) Token.closure elem', ctxt') end
-
-fun activate raw_elem ctxt =
-  let val elem = raw_elem |> Element.map_ctxt
-   {binding = I,
-    typ = I,
-    term = I,
-    pattern = I,
-    fact = Proof_Context.get_fact ctxt,
-    attrib = Attrib.check_src ctxt}
-  in activate_i elem ctxt end
-
-in
-
-val read_goal_statement = prep_statement read_full_context_statement activate
-
-end
-
-
-(* Proof assumption command *)
-
-local
-
-val structured_statement =
-  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
-    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows))
-
-fun these_factss more_facts (named_factss, state) =
-  (named_factss, state |> Proof.set_facts (maps snd named_factss @ more_facts))
-
-fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state =
-  let
-    val ctxt = Proof.context_of state;
-
-    val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
-    val {fixes = params, assumes = prems_propss, shows = concl_propss, result_binds, text, ...} =
-      #1 (prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt);
-    val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
-  in
-    state
-    |> Proof.assert_forward
-    |> Proof.map_context_result (fn ctxt =>
-      ctxt
-      |> Proof_Context.augment text
-      |> fold Variable.maybe_bind_term result_binds
-      |> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss
-      |-> (fn premss => fn ctxt =>
-            (premss, Context_Facts.register_facts (flat premss) ctxt))
-      |-> (fn premss =>
-        Proof_Context.note_thmss "" (bindings ~~ (map o map) (fn th => ([th], [])) premss)))
-    |> these_factss [] |> #2
-  end
-
-val assume =
-  gen_assume Proof_Context.cert_statement (K I) Assumption.assume_export
-
-in
-
-val _ = Outer_Syntax.command \<^command_keyword>\<open>assuming\<close> "elaborated assumption"
-  (structured_statement >> (fn (a, b, c) => Toplevel.proof (fn state =>
-    let
-      val ctxt = Proof.context_of state
-
-      fun read_option_typ NONE = NONE
-        | read_option_typ (SOME s) = SOME (Syntax.read_typ ctxt s)
-      fun read_terms (s, ss) =
-        let val f = Syntax.read_term ctxt in (f s, map f ss) end
-
-      val a' = map (fn (b, s, m) => (b, read_option_typ s, m)) a
-      val b' = map (map read_terms) b
-      val c' = c |> map (fn ((b, atts), ss) =>
-        ((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss))
-      val c'' = Elab.elaborate ctxt [] c'
-    in assume a' b' c'' state end)))
-
-end
-
-
-end
\ No newline at end of file
diff --git a/spartan/core/elaboration.ML b/spartan/core/elaboration.ML
deleted file mode 100644
index 9e5e0bd..0000000
--- a/spartan/core/elaboration.ML
+++ /dev/null
@@ -1,91 +0,0 @@
-(*  Title:      elaboration.ML
-    Author:     Joshua Chen
-
-Basic term elaboration.
-*)
-
-structure Elab: sig
-
-val elab: Proof.context -> cterm list -> term -> Envir.env
-val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term
-val elaborate: Proof.context -> cterm list -> ('a * (term * term list) list) list -> ('a * (term * term list) list) list
-
-end = struct
-
-(*Elaborate `tm` by solving the inference problem `tm: {}`, knowing `assums`,
-  which are fully elaborated, in `ctxt`. Return a substitution.*)
-fun elab ctxt assums tm =
-  if Lib.no_vars tm
-  then Envir.init
-  else
-    let
-      val inf = Goal.init (Thm.cterm_of ctxt (Lib.typing_of_term tm))
-      val res = Types.check_infer (map Thm.assume assums) 1 (ctxt, inf)
-      val tm' =
-        Thm.prop_of (#2 (Seq.hd (Seq.filter_results res)))
-        |> Lib.dest_prop |> Lib.term_of_typing
-        handle TERM ("dest_typing", [t]) =>
-          let val typ = Logic.unprotect (Logic.strip_assums_concl t)
-            |> Lib.term_of_typing
-          in
-            error ("Elaboration of " ^ Syntax.string_of_term ctxt typ ^ " failed")
-          end
-    in
-      Seq.hd (Unify.matchers (Context.Proof ctxt) [(tm, tm')])
-    end
-    handle Option => error
-      ("Elaboration of " ^ Syntax.string_of_term ctxt tm ^ " failed")
-
-(*Recursively elaborate a statement \<And>x ... y. \<lbrakk>...\<rbrakk> \<Longrightarrow> P x ... y by elaborating
-  only the types of typing judgments (in particular, does not look at judgmental
-  equality statements). Could also elaborate the terms of typing judgments, but
-  for now we assume that these are always free variables in all the cases we're
-  interested in.*)
-fun elab_stmt ctxt assums stmt =
-  let
-    val stmt = Lib.dest_prop stmt
-    fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
-  in
-    if Lib.no_vars stmt orelse Lib.is_eq stmt then
-      (Envir.init, stmt)
-    else if Lib.is_typing stmt then
-      let
-        val typ = Lib.type_of_typing stmt
-        val subst = elab ctxt assums typ
-      in (subst, subst_term subst stmt) end
-    else
-      let
-        fun elab' assums (x :: xs) =
-              let
-                val (env, x') = elab_stmt ctxt assums x
-                val assums' =
-                  if Lib.no_vars x' then Thm.cterm_of ctxt x' :: assums else assums
-              in env :: elab' assums' xs end
-          | elab' _ [] = []
-        val (prems, concl) = Lib.decompose_goal ctxt stmt
-        val subst = fold (curry Envir.merge) (elab' assums prems) Envir.init
-        val prems' = map (Thm.cterm_of ctxt o subst_term subst) prems
-        val subst' =
-          if Lib.is_typing concl then
-            let val typ = Lib.type_of_typing concl
-            in Envir.merge (subst, elab ctxt (assums @ prems') typ) end
-          else subst
-      in (subst', subst_term subst' stmt) end
-  end
-
-(*Apply elaboration to the list format that assumptions and goal statements are
-  given in*)
-fun elaborate ctxt known assms =
-  let
-    fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
-    fun elab_fact (fact, xs) assums =
-      let val (subst, fact') = elab_stmt ctxt assums fact in
-        ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums)
-      end
-    fun elab (b, facts) assums =
-      let val (facts', assums') = fold_map elab_fact facts assums
-      in ((b, facts'), assums') end
-  in #1 (fold_map elab assms known) end
-
-
-end
diff --git a/spartan/core/elimination.ML b/spartan/core/elimination.ML
deleted file mode 100644
index cf9d21e..0000000
--- a/spartan/core/elimination.ML
+++ /dev/null
@@ -1,48 +0,0 @@
-(*  Title:      elimination.ML
-    Author:     Joshua Chen
-
-Type elimination setup.
-*)
-
-structure Elim: sig
-
-val Rules: Proof.context -> (thm * indexname list) Termtab.table
-val rules: Proof.context -> (thm * indexname list) list
-val lookup_rule: Proof.context -> Termtab.key -> (thm * indexname list) option
-val register_rule: term list -> thm -> Context.generic -> Context.generic
-
-end = struct
-
-(** Context data **)
-
-(* Elimination rule data *)
-
-(*Stores elimination rules together with a list of the indexnames of the
-  variables each rule eliminates. Keyed by head of the type being eliminated.*)
-structure Rules = Generic_Data (
-  type T = (thm * indexname list) Termtab.table
-  val empty = Termtab.empty
-  val extend = I
-  val merge = Termtab.merge (eq_fst Thm.eq_thm_prop)
-)
-
-val Rules = Rules.get o Context.Proof
-fun rules ctxt = map (op #2) (Termtab.dest (Rules ctxt))
-fun lookup_rule ctxt = Termtab.lookup (Rules ctxt)
-fun register_rule tms rl =
-  let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl))
-  in Rules.map (Termtab.update (hd, (rl, map (#1 o dest_Var) tms))) end
-
-
-(* [elim] attribute *)
-val _ = Theory.setup (
-  Attrib.setup \<^binding>\<open>elim\<close>
-    (Scan.repeat Args.term_pattern >>
-      (Thm.declaration_attribute o register_rule))
-    ""
-  #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elim\<close>,
-      fn context => map #1 (rules (Context.proof_of context)))
-)
-
-
-end
diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML
deleted file mode 100644
index 5ae8c73..0000000
--- a/spartan/core/eqsubst.ML
+++ /dev/null
@@ -1,442 +0,0 @@
-(*  Title:      eqsubst.ML
-    Author:     Lucas Dixon, University of Edinburgh
-    Modified:   Joshua Chen, University of Innsbruck
-
-Perform a substitution using an equation.
-
-This code is slightly modified from the original at Tools/eqsubst..ML,
-to incorporate auto-typechecking for type theory.
-*)
-
-signature EQSUBST =
-sig
-  type match =
-    ((indexname * (sort * typ)) list (* type instantiations *)
-      * (indexname * (typ * term)) list) (* term instantiations *)
-    * (string * typ) list (* fake named type abs env *)
-    * (string * typ) list (* type abs env *)
-    * term (* outer term *)
-
-  type searchinfo =
-    Proof.context
-    * int (* maxidx *)
-    * Zipper.T (* focusterm to search under *)
-
-  datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq
-
-  val skip_first_asm_occs_search: ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> int -> 'b -> 'c skipseq
-  val skip_first_occs_search: int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
-  val skipto_skipseq: int -> 'a Seq.seq Seq.seq -> 'a skipseq
-
-  (* tactics *)
-  val eqsubst_asm_tac: Proof.context -> int list -> thm list -> int -> tactic
-  val eqsubst_asm_tac': Proof.context ->
-    (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic
-  val eqsubst_tac: Proof.context ->
-    int list -> (* list of occurrences to rewrite, use [0] for any *)
-    thm list -> int -> tactic
-  val eqsubst_tac': Proof.context ->
-    (searchinfo -> term -> match Seq.seq) (* search function *)
-    -> thm (* equation theorem to rewrite with *)
-    -> int (* subgoal number in goal theorem *)
-    -> thm (* goal theorem *)
-    -> thm Seq.seq (* rewritten goal theorem *)
-
-  (* search for substitutions *)
-  val valid_match_start: Zipper.T -> bool
-  val search_lr_all: Zipper.T -> Zipper.T Seq.seq
-  val search_lr_valid: (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
-  val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
-  val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
-  val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
-end;
-
-structure EqSubst: EQSUBST =
-struct
-
-(* changes object "=" to meta "==" which prepares a given rewrite rule *)
-fun prep_meta_eq ctxt =
-  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
-
-(* make free vars into schematic vars with index zero *)
-fun unfix_frees frees =
-   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
-
-
-type match =
-  ((indexname * (sort * typ)) list (* type instantiations *)
-   * (indexname * (typ * term)) list) (* term instantiations *)
-  * (string * typ) list (* fake named type abs env *)
-  * (string * typ) list (* type abs env *)
-  * term; (* outer term *)
-
-type searchinfo =
-  Proof.context
-  * int (* maxidx *)
-  * Zipper.T; (* focusterm to search under *)
-
-
-(* skipping non-empty sub-sequences but when we reach the end
-   of the seq, remembering how much we have left to skip. *)
-datatype 'a skipseq =
-  SkipMore of int |
-  SkipSeq of 'a Seq.seq Seq.seq;
-
-(* given a seqseq, skip the first m non-empty seq's, note deficit *)
-fun skipto_skipseq m s =
-  let
-    fun skip_occs n sq =
-      (case Seq.pull sq of
-        NONE => SkipMore n
-      | SOME (h, t) =>
-        (case Seq.pull h of
-          NONE => skip_occs n t
-        | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
-  in skip_occs m s end;
-
-(* note: outerterm is the taget with the match replaced by a bound
-   variable : ie: "P lhs" beocmes "%x. P x"
-   insts is the types of instantiations of vars in lhs
-   and typinsts is the type instantiations of types in the lhs
-   Note: Final rule is the rule lifted into the ontext of the
-   taget thm. *)
-fun mk_foo_match mkuptermfunc Ts t =
-  let
-    val ty = Term.type_of t
-    val bigtype = rev (map snd Ts) ---> ty
-    fun mk_foo 0 t = t
-      | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
-    val num_of_bnds = length Ts
-    (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
-    val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
-  in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end;
-
-(* T is outer bound vars, n is number of locally bound vars *)
-(* THINK: is order of Ts correct...? or reversed? *)
-fun mk_fake_bound_name n = ":b_" ^ n;
-fun fakefree_badbounds Ts t =
-  let val (FakeTs, Ts, newnames) =
-    fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) =>
-      let
-        val newname = singleton (Name.variant_list usednames) n
-      in
-        ((mk_fake_bound_name newname, ty) :: FakeTs,
-          (newname, ty) :: Ts,
-          newname :: usednames)
-      end) Ts ([], [], [])
-  in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
-
-(* before matching we need to fake the bound vars that are missing an
-   abstraction. In this function we additionally construct the
-   abstraction environment, and an outer context term (with the focus
-   abstracted out) for use in rewriting with RW_Inst.rw *)
-fun prep_zipper_match z =
-  let
-    val t = Zipper.trm z
-    val c = Zipper.ctxt z
-    val Ts = Zipper.C.nty_ctxt c
-    val (FakeTs', Ts', t') = fakefree_badbounds Ts t
-    val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
-  in
-    (t', (FakeTs', Ts', absterm))
-  end;
-
-(* Unification with exception handled *)
-(* given context, max var index, pat, tgt; returns Seq of instantiations *)
-fun clean_unify ctxt ix (a as (pat, tgt)) =
-  let
-    (* type info will be re-derived, maybe this can be cached
-       for efficiency? *)
-    val pat_ty = Term.type_of pat;
-    val tgt_ty = Term.type_of tgt;
-    (* FIXME is it OK to ignore the type instantiation info?
-       or should I be using it? *)
-    val typs_unify =
-      SOME (Sign.typ_unify (Proof_Context.theory_of ctxt) (pat_ty, tgt_ty) (Vartab.empty, ix))
-        handle Type.TUNIFY => NONE;
-  in
-    (case typs_unify of
-      SOME (typinsttab, ix2) =>
-        let
-          (* FIXME is it right to throw away the flexes?
-             or should I be using them somehow? *)
-          fun mk_insts env =
-            (Vartab.dest (Envir.type_env env),
-             Vartab.dest (Envir.term_env env));
-          val initenv =
-            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
-          val useq = Unify.smash_unifiers (Context.Proof ctxt) [a] initenv
-            handle ListPair.UnequalLengths => Seq.empty
-              | Term.TERM _ => Seq.empty;
-          fun clean_unify' useq () =
-            (case (Seq.pull useq) of
-               NONE => NONE
-             | SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
-            handle ListPair.UnequalLengths => NONE
-              | Term.TERM _ => NONE;
-        in
-          (Seq.make (clean_unify' useq))
-        end
-    | NONE => Seq.empty)
-  end;
-
-(* Unification for zippers *)
-(* Note: Ts is a modified version of the original names of the outer
-   bound variables. New names have been introduced to make sure they are
-   unique w.r.t all names in the term and each other. usednames' is
-   oldnames + new names. *)
-fun clean_unify_z ctxt maxidx pat z =
-  let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
-    Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
-      (clean_unify ctxt maxidx (t, pat))
-  end;
-
-
-fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l
-  | bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t
-  | bot_left_leaf_of x = x;
-
-(* Avoid considering replacing terms which have a var at the head as
-   they always succeed trivially, and uninterestingly. *)
-fun valid_match_start z =
-  (case bot_left_leaf_of (Zipper.trm z) of
-    Var _ => false
-  | _ => true);
-
-(* search from top, left to right, then down *)
-val search_lr_all = ZipperSearch.all_bl_ur;
-
-(* search from top, left to right, then down *)
-fun search_lr_valid validf =
-  let
-    fun sf_valid_td_lr z =
-      let val here = if validf z then [Zipper.Here z] else [] in
-        (case Zipper.trm z of
-          _ $ _ =>
-            [Zipper.LookIn (Zipper.move_down_left z)] @ here @
-            [Zipper.LookIn (Zipper.move_down_right z)]
-        | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
-        | _ => here)
-      end;
-  in Zipper.lzy_search sf_valid_td_lr end;
-
-(* search from bottom to top, left to right *)
-fun search_bt_valid validf =
-  let
-    fun sf_valid_td_lr z =
-      let val here = if validf z then [Zipper.Here z] else [] in
-        (case Zipper.trm z of
-          _ $ _ =>
-            [Zipper.LookIn (Zipper.move_down_left z),
-             Zipper.LookIn (Zipper.move_down_right z)] @ here
-        | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
-        | _ => here)
-      end;
-  in Zipper.lzy_search sf_valid_td_lr end;
-
-fun searchf_unify_gen f (ctxt, maxidx, z) lhs =
-  Seq.map (clean_unify_z ctxt maxidx lhs) (Zipper.limit_apply f z);
-
-(* search all unifications *)
-val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
-
-(* search only for 'valid' unifiers (non abs subterms and non vars) *)
-val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start);
-
-val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start);
-
-(* apply a substitution in the conclusion of the theorem *)
-(* cfvs are certified free var placeholders for goal params *)
-(* conclthm is a theorem of for just the conclusion *)
-(* m is instantiation/match information *)
-(* rule is the equation for substitution *)
-fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
-  RW_Inst.rw ctxt m rule conclthm
-  |> unfix_frees cfvs
-  |> Conv.fconv_rule Drule.beta_eta_conversion
-  |> (fn r => resolve_tac ctxt [r] i st);
-
-(* substitute within the conclusion of goal i of gth, using a meta
-equation rule. Note that we assume rule has var indicies zero'd *)
-fun prep_concl_subst ctxt i gth =
-  let
-    val th = Thm.incr_indexes 1 gth;
-    val tgt_term = Thm.prop_of th;
-
-    val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
-    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
-
-    val conclterm = Logic.strip_imp_concl fixedbody;
-    val conclthm = Thm.trivial (Thm.cterm_of ctxt conclterm);
-    val maxidx = Thm.maxidx_of th;
-    val ft =
-      (Zipper.move_down_right (* ==> *)
-       o Zipper.move_down_left (* Trueprop *)
-       o Zipper.mktop
-       o Thm.prop_of) conclthm
-  in
-    ((cfvs, conclthm), (ctxt, maxidx, ft))
-  end;
-
-(* substitute using an object or meta level equality *)
-fun eqsubst_tac' ctxt searchf instepthm i st =
-  let
-    val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st;
-    val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
-    fun rewrite_with_thm r =
-      let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in
-        searchf searchinfo lhs
-        |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r)
-      end;
-  in stepthms |> Seq.maps rewrite_with_thm end;
-
-
-(* General substitution of multiple occurrences using one of
-   the given theorems *)
-
-fun skip_first_occs_search occ srchf sinfo lhs =
-  (case skipto_skipseq occ (srchf sinfo lhs) of
-    SkipMore _ => Seq.empty
-  | SkipSeq ss => Seq.flat ss);
-
-(* The "occs" argument is a list of integers indicating which occurrence
-w.r.t. the search order, to rewrite. Backtracking will also find later
-occurrences, but all earlier ones are skipped. Thus you can use [0] to
-just find all rewrites. *)
-
-fun eqsubst_tac ctxt occs thms i st =
-  let val nprems = Thm.nprems_of st in
-    if nprems < i then Seq.empty else
-    let
-      val thmseq = Seq.of_list thms;
-      fun apply_occ occ st =
-        thmseq |> Seq.maps (fn r =>
-          eqsubst_tac' ctxt
-            (skip_first_occs_search occ searchf_lr_unify_valid) r
-            (i + (Thm.nprems_of st - nprems)) st);
-      val sorted_occs = Library.sort (rev_order o int_ord) occs;
-    in
-      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
-    end
-  end;
-
-
-(* apply a substitution inside assumption j, keeps asm in the same place *)
-fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) =
-  let
-    val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
-    val preelimrule =
-      RW_Inst.rw ctxt m rule pth
-      |> (Seq.hd o prune_params_tac ctxt)
-      |> Thm.permute_prems 0 ~1 (* put old asm first *)
-      |> unfix_frees cfvs (* unfix any global params *)
-      |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
-  in
-    (* ~j because new asm starts at back, thus we subtract 1 *)
-    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
-      (dresolve_tac ctxt [preelimrule] i st2)
-  end;
-
-
-(* prepare to substitute within the j'th premise of subgoal i of gth,
-using a meta-level equation. Note that we assume rule has var indicies
-zero'd. Note that we also assume that premt is the j'th premice of
-subgoal i of gth. Note the repetition of work done for each
-assumption, i.e. this can be made more efficient for search over
-multiple assumptions.  *)
-fun prep_subst_in_asm ctxt i gth j =
-  let
-    val th = Thm.incr_indexes 1 gth;
-    val tgt_term = Thm.prop_of th;
-
-    val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
-    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
-
-    val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
-    val asm_nprems = length (Logic.strip_imp_prems asmt);
-
-    val pth = Thm.trivial ((Thm.cterm_of ctxt) asmt);
-    val maxidx = Thm.maxidx_of th;
-
-    val ft =
-      (Zipper.move_down_right (* trueprop *)
-         o Zipper.mktop
-         o Thm.prop_of) pth
-  in ((cfvs, j, asm_nprems, pth), (ctxt, maxidx, ft)) end;
-
-(* prepare subst in every possible assumption *)
-fun prep_subst_in_asms ctxt i gth =
-  map (prep_subst_in_asm ctxt i gth)
-    ((fn l => Library.upto (1, length l))
-      (Logic.prems_of_goal (Thm.prop_of gth) i));
-
-
-(* substitute in an assumption using an object or meta level equality *)
-fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i st =
-  let
-    val asmpreps = prep_subst_in_asms ctxt i st;
-    val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
-    fun rewrite_with_thm r =
-      let
-        val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
-        fun occ_search occ [] = Seq.empty
-          | occ_search occ ((asminfo, searchinfo)::moreasms) =
-              (case searchf searchinfo occ lhs of
-                SkipMore i => occ_search i moreasms
-              | SkipSeq ss =>
-                  Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
-                    (occ_search 1 moreasms)) (* find later substs also *)
-      in
-        occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i st r)
-      end;
-  in stepthms |> Seq.maps rewrite_with_thm end;
-
-
-fun skip_first_asm_occs_search searchf sinfo occ lhs =
-  skipto_skipseq occ (searchf sinfo lhs);
-
-fun eqsubst_asm_tac ctxt occs thms i st =
-  let val nprems = Thm.nprems_of st in
-    if nprems < i then Seq.empty
-    else
-      let
-        val thmseq = Seq.of_list thms;
-        fun apply_occ occ st =
-          thmseq |> Seq.maps (fn r =>
-            eqsubst_asm_tac' ctxt
-              (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
-              (i + (Thm.nprems_of st - nprems)) st);
-        val sorted_occs = Library.sort (rev_order o int_ord) occs;
-      in
-        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
-      end
-  end;
-
-(* combination method that takes a flag (true indicates that subst
-   should be done to an assumption, false = apply to the conclusion of
-   the goal) as well as the theorems to use *)
-val _ =
-  let
-    val parser =
-      Scan.lift (Args.mode "asm"
-        -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0])
-      -- Attrib.thms
-    fun eqsubst_asm_ctac occs inthms =
-      CONTEXT_TACTIC' (fn ctxt => eqsubst_asm_tac ctxt occs inthms)
-    fun eqsubst_ctac occs inthms =
-      CONTEXT_TACTIC' (fn ctxt => eqsubst_tac ctxt occs inthms)
-  in
-    Theory.setup (
-      Method.setup \<^binding>\<open>sub\<close>
-        (parser >> (fn ((asm, occs), inthms) => fn ctxt => SIMPLE_METHOD' (
-          (if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
-        "single-step substitution" (* #>
-      Method.setup \<^binding>\<open>subst\<close>
-        (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD (
-          CHEADGOAL o SIDE_CONDS 0
-            ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms)))))
-        "single-step substitution with automatic discharge of side conditions" *)
-    )
-  end
-
-end;
diff --git a/spartan/core/equality.ML b/spartan/core/equality.ML
deleted file mode 100644
index 023147b..0000000
--- a/spartan/core/equality.ML
+++ /dev/null
@@ -1,90 +0,0 @@
-(*  Title:      equality.ML
-    Author:     Joshua Chen
-
-Equality reasoning with identity types.
-*)
-
-structure Equality:
-sig
-
-val dest_Id: term -> term * term * term
-
-val push_hyp_tac: term * term -> Proof.context -> int -> tactic
-val induction_tac: term -> term -> term -> term -> Proof.context -> tactic
-val equality_context_tac: Facts.ref -> Proof.context -> context_tactic
-
-end = struct
-
-fun dest_Id tm = case tm of
-    Const (\<^const_name>\<open>Id\<close>, _) $ A $ x $ y => (A, x, y)
-  | _ => error "dest_Id"
-
-(*Context assumptions that have already been pushed into the type family*)
-structure Inserts = Proof_Data (
-  type T = term Item_Net.T
-  val init = K (Item_Net.init Term.aconv_untyped single)
-)
-
-fun push_hyp_tac (t, _) =
-  Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl, ...} =>
-    let
-      val (_, C) = Lib.dest_typing (Thm.term_of concl)
-      val B = Thm.cterm_of ctxt (Lib.lambda_var t C)
-      val a = Thm.cterm_of ctxt t
-      (*The resolvent is PiE[where ?B=B and ?a=a]*)
-      val resolvent =
-        Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
-    in
-      HEADGOAL (resolve_tac ctxt [resolvent])
-      THEN SOMEGOAL (known_tac ctxt)
-    end)
-
-fun induction_tac p A x y ctxt =
-  let
-    val [p, A, x, y] = map (Thm.cterm_of ctxt) [p, A, x, y]
-  in
-    HEADGOAL (resolve_tac ctxt
-      [Drule.infer_instantiate' ctxt [SOME p, SOME A, SOME x, SOME y] @{thm IdE}])
-  end
-
-val side_conds_tac = TRY oo typechk_tac
-
-fun equality_context_tac fact ctxt =
-  let
-    val eq_th = Proof_Context.get_fact_single ctxt fact
-    val (p, (A, x, y)) = (Lib.dest_typing ##> dest_Id) (Thm.prop_of eq_th)
-
-    val hyps =
-      Facts.props (Proof_Context.facts_of ctxt)
-      |> filter (fn (th, _) => Lib.is_typing (Thm.prop_of th))
-      |> map (Lib.dest_typing o Thm.prop_of o fst)
-      |> filter_out (fn (t, _) =>
-          Term.aconv (t, p) orelse Item_Net.member (Inserts.get ctxt) t)
-      |> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct [p, x, y] T))
-      |> filter (fn (_, i) => i > 0)
-      (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
-        If they are incomparable, then order by decreasing
-        `subterm_count [p, x, y] T`*)
-      |> sort (fn (((t1, _), i), ((_, T2), j)) =>
-          Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
-      |> map #1
-
-    val record_inserts =
-      Inserts.map (fold (fn (t, _) => fn net => Item_Net.update t net) hyps)
-
-    val tac =
-      fold (fn hyp => fn tac => tac THEN HEADGOAL (push_hyp_tac hyp ctxt))
-        hyps all_tac
-      THEN (
-        induction_tac p A x y ctxt
-        THEN RANGE (replicate 3 (typechk_tac ctxt) @ [side_conds_tac ctxt]) 1
-      )
-      THEN (
-        REPEAT_DETERM_N (length hyps) (SOMEGOAL (resolve_tac ctxt @{thms PiI}))
-        THEN ALLGOALS (side_conds_tac ctxt)
-      )
-  in
-    fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT (record_inserts ctxt) (tac st)
-  end
-
-end
diff --git a/spartan/core/focus.ML b/spartan/core/focus.ML
deleted file mode 100644
index b963cfe..0000000
--- a/spartan/core/focus.ML
+++ /dev/null
@@ -1,158 +0,0 @@
-(*  Title:      focus.ML
-    Author:     Joshua Chen
-
-Focus on head subgoal, with optional variable renaming.
-
-Modified from code contained in ~~/Pure/Isar/subgoal.ML.
-*)
-
-local
-
-fun reverse_prems imp =
-  let val (prems, concl) = (Drule.strip_imp_prems imp, Drule.strip_imp_concl imp)
-  in fold (curry mk_implies) prems concl end
-
-fun gen_focus ctxt i bindings raw_st =
-  let
-    val st = raw_st
-      |> Thm.solve_constraints
-      |> Thm.transfer' ctxt
-      |> Raw_Simplifier.norm_hhf_protect ctxt
-
-    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt
-
-    val ((params, goal), ctxt2) =
-      Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1
-
-    val (asms, concl) =
-      (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
-
-    fun intern_var_assms asm (asms, concl) =
-      if Lib.no_vars (Thm.term_of asm)
-      then (asm :: asms, concl)
-      else (asms, Drule.mk_implies (asm, concl))
-
-    val (asms', concl') = fold intern_var_assms asms ([], concl)
-      |> apfst rev |> apsnd reverse_prems
-
-    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of (asms')) ctxt2
-    val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst)
-    val schematics = (schematic_types, schematic_terms)
-    val asms' = map (Thm.instantiate_cterm schematics) asms'
-    val concl' = Thm.instantiate_cterm schematics concl'
-    val (prems, context) = Assumption.add_assumes asms' ctxt3
-  in
-    ({context = context, params = params, prems = prems,
-      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
-  end
-
-fun param_bindings ctxt (param_suffix, raw_param_specs) st =
-  let
-    val _ = if Thm.no_prems st then error "No subgoals!" else ()
-    val subgoal = #1 (Logic.dest_implies (Thm.prop_of st))
-    val subgoal_params =
-      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
-      |> Term.variant_frees subgoal |> map #1
-
-    val n = length subgoal_params
-    val m = length raw_param_specs
-    val _ =
-      m <= n orelse
-        error ("Excessive subgoal parameter specification" ^
-          Position.here_list (map snd (drop n raw_param_specs)))
-
-    val param_specs = raw_param_specs
-      |> map
-        (fn (NONE, _) => NONE
-          | (SOME x, pos) =>
-              let
-                val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
-                val _ = Variable.check_name b
-              in SOME b end)
-      |> param_suffix ? append (replicate (n - m) NONE)
-
-    fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys
-      | bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys
-      | bindings _ ys = map Binding.name ys
-  in bindings param_specs subgoal_params end
-
-fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state =
-  let
-    val _ = Proof.assert_backward state
-
-    val state1 = state
-      |> Proof.map_context (Proof_Context.set_mode Proof_Context.mode_schematic)
-      |> Proof.refine_insert []
-
-    val {context = ctxt, facts, goal = st} = Proof.raw_goal state1
-    val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding
-
-    val subgoal_focus = #1
-      (gen_focus ctxt 1 (SOME (param_bindings ctxt param_specs st)) st)
-
-    val prems = #prems subgoal_focus
-
-    fun after_qed (ctxt'', [[result]]) =
-      Proof.end_block #> (fn state' =>
-        let
-          val ctxt' = Proof.context_of state'
-          val results' =
-            Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result)
-        in
-          state'
-          |> Proof.refine_primitive (fn _ => fn _ =>
-            Subgoal.retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
-              (Goal.protect 0 result) st
-            |> Seq.hd)
-          |> Proof.map_context
-            (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
-        end)
-      #> Proof.reset_facts
-      #> Proof.enter_backward
-  in
-    state1
-    |> Proof.enter_forward
-    |> Proof.using_facts []
-    |> Proof.begin_block
-    |> Proof.map_context (fn _ =>
-      #context subgoal_focus
-      |> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])]
-      |> snd
-      |> Context_Facts.register_facts prems)
-    |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
-        NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])]
-    |> #2
-    |> Proof.using_facts (facts @ prems)
-    |> pair subgoal_focus
-  end
-
-val opt_fact_binding =
-  Scan.optional ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Args.colon)
-    Binding.empty_atts
-
-val for_params = Scan.optional
-  (\<^keyword>\<open>vars\<close> |--
-    Parse.!!! ((Scan.option Parse.dots >> is_some) --
-      (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
-  (false, [])
-
-val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd
-
-val parser = opt_fact_binding -- for_params >> (fn (fact, params) =>
-  Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd fact params))
-
-in
-
-(** Outer syntax commands **)
-
-val _ = Outer_Syntax.command \<^command_keyword>\<open>focus\<close>
-  "focus on first subgoal within backward refinement, without instantiating schematic vars"
-  parser
-
-val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^item>\<close> "focus bullet" parser
-val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^enum>\<close> "focus bullet" parser
-val _ = Outer_Syntax.command \<^command_keyword>\<open>\<circ>\<close> "focus bullet" parser
-val _ = Outer_Syntax.command \<^command_keyword>\<open>\<diamondop>\<close> "focus bullet" parser
-val _ = Outer_Syntax.command \<^command_keyword>\<open>~\<close> "focus bullet" parser
-
-end
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
deleted file mode 100644
index 7d52495..0000000
--- a/spartan/core/goals.ML
+++ /dev/null
@@ -1,213 +0,0 @@
-(*  Title:      goals.ML
-    Author:     Joshua Chen
-
-Goal statements and proof term export.
-
-Modified from code contained in ~~/Pure/Isar/specification.ML.
-*)
-
-local
-
-val long_keyword =
-  Parse_Spec.includes >> K "" ||
-  Parse_Spec.long_statement_keyword
-
-val long_statement =
-  Scan.optional
-    (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword)
-    Binding.empty_atts
-  -- Scan.optional Parse_Spec.includes []
-  -- Parse_Spec.long_statement >>
-    (fn ((binding, includes), (elems, concl)) =>
-      (true, binding, includes, elems, concl))
-
-val short_statement =
-  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >>
-    (fn ((shows, assumes), fixes) =>
-      (false, Binding.empty_atts, [],
-      [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)
-    )
-
-fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
-  let
-    val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt
-    val prems = Assumption.local_prems_of elems_ctxt ctxt
-    val stmt_ctxt =
-      fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt
-  in case raw_stmt
-    of Element.Shows _ =>
-        let val stmt' = Attrib.map_specs (map prep_att) stmt
-        in (([], prems, stmt', NONE), stmt_ctxt) end
-    | Element.Obtains raw_obtains =>
-        let
-          val asms_ctxt = stmt_ctxt
-            |> fold (fn ((name, _), asm) =>
-                snd o Proof_Context.add_assms Assumption.assume_export
-                  [((name, [Context_Rules.intro_query NONE]), asm)]) stmt
-          val that = Assumption.local_prems_of asms_ctxt stmt_ctxt
-          val ([(_, that')], that_ctxt) = asms_ctxt
-            |> Proof_Context.set_stmt true
-            |> Proof_Context.note_thmss ""
-                [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
-            ||> Proof_Context.restore_stmt asms_ctxt
-          val stmt' =
-            [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])]
-        in
-          ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'),
-          that_ctxt)
-        end
-  end
-
-fun define_proof_term name (local_name, [th]) lthy =
-      let
-        fun make_name_binding suffix local_name =
-          let val base_local_name = Long_Name.base_name local_name
-          in Binding.qualified_name
-            ((case base_local_name of "" => name | _ => base_local_name) ^
-             (case suffix
-              of SOME "prf" => "_prf"
-              | SOME "def" => "_def"
-              | _ => ""))
-          end
-
-        val (prems, concl) =
-          (Logic.strip_assums_hyp (Thm.prop_of th),
-           Logic.strip_assums_concl (Thm.prop_of th))
-      in
-        if not (Lib.is_typing concl) then ([], lthy)
-        else let
-          val prems_vars = distinct Term.aconv (flat
-            (map (Lib.collect_subterms is_Var) prems))
-
-          val concl_vars = Lib.collect_subterms is_Var
-            (Lib.term_of_typing concl)
-
-          val params = inter Term.aconv concl_vars prems_vars
-
-          val prf_tm = fold_rev lambda params (Lib.term_of_typing concl)
-
-          val ((_, (_, raw_def)), lthy') = Local_Theory.define
-            ((make_name_binding NONE local_name, Mixfix.NoSyn),
-            ((make_name_binding (SOME "prf") local_name, []), prf_tm)) lthy
-
-          val def = fold
-            (fn th1 => fn th2 => Thm.combination th2 th1)
-            (map (Thm.reflexive o Thm.cterm_of lthy) params)
-            raw_def
-
-          val ((_, def'), lthy'') = Local_Theory.note
-            ((make_name_binding (SOME "def") local_name, []), [def])
-            lthy'
-        in
-          (def', lthy'')
-        end
-      end
-  | define_proof_term _ _ _ = error
-      ("Unimplemented: proof terms for multiple facts in one statement")
-
-fun gen_schematic_theorem
-  bundle_includes prep_att prep_stmt
-  gen_prf_tm long kind
-  before_qed after_qed
-  (name, raw_atts) raw_includes raw_elems raw_concl
-  do_print lthy
-  =
-  let
-    val _ = Local_Theory.assert lthy
-    val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy))
-    val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
-      |> bundle_includes raw_includes
-      |> prep_statement (prep_att lthy) prep_stmt elems raw_concl
-    val atts = more_atts @ map (prep_att lthy) raw_atts
-    val pos = Position.thread_data ()
-    val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN
-
-    fun gen_and_after_qed results goal_ctxt' =
-      let
-        val results' = burrow
-          (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy)
-          results
-
-        val ((res, lthy'), substmts) =
-          if forall (Binding.is_empty_atts o fst) stmt
-          then ((map (pair "") results', lthy), false)
-          else
-            (Local_Theory.notes_kind kind
-              (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results')
-              lthy,
-            true)
-
-        val (res', lthy'') =
-          if gen_prf_tm
-          then
-            let
-              val (prf_tm_defs, new_lthy) = fold
-                (fn result => fn (defs, lthy) =>
-                  apfst (fn new_defs => defs @ new_defs)
-                    (define_proof_term (Binding.name_of name) result lthy))
-                res
-                ([], lthy')
-              val res_folded =
-                map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res
-            in
-              Local_Theory.notes_kind kind
-                [((name, @{attributes [type]} @ atts),
-                  [(maps #2 res_folded, [])])]
-                new_lthy
-            end
-          else
-            Local_Theory.notes_kind kind
-              [((name, atts), [(maps #2 res, [])])]
-              lthy'
-
-        val _ = Proof_Display.print_results do_print pos lthy''
-            ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')
-
-        val _ =
-          if substmts then map
-            (fn (name, ths) => Proof_Display.print_results do_print pos lthy''
-              (("and", name), [("", ths)]))
-            res
-          else []
-      in
-        after_qed results' lthy''
-      end
-  in
-    goal_ctxt
-    |> not (null prems) ?
-      (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])]
-        #> snd #> Context_Facts.register_facts prems)
-    |> Proof.theorem before_qed gen_and_after_qed (map snd stmt)
-    |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
-  end
-
-val schematic_theorem_cmd =
-  gen_schematic_theorem
-    Bundle.includes_cmd
-    Attrib.check_src
-    Elaborated_Statement.read_goal_statement
-
-fun theorem spec descr =
-  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
-    (Scan.option (Args.parens (Args.$$$ "def"))
-      -- (long_statement || short_statement) >>
-        (fn (opt_derive, (long, binding, includes, elems, concl)) =>
-          schematic_theorem_cmd
-            (case opt_derive of SOME "def" => true | _ => false)
-            long descr NONE (K I) binding includes elems concl))
-
-fun definition spec descr =
-  Outer_Syntax.local_theory_to_proof' spec "definition via proof"
-    ((long_statement || short_statement) >>
-      (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd
-        true long descr NONE (K I) binding includes elems concl))
-
-in
-
-val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem"
-val _ = theorem \<^command_keyword>\<open>Lemma\<close> "Lemma"
-val _ = theorem \<^command_keyword>\<open>Corollary\<close> "Corollary"
-val _ = theorem \<^command_keyword>\<open>Proposition\<close> "Proposition"
-val _ = definition \<^command_keyword>\<open>Definition\<close> "Definition"
-
-end
diff --git a/spartan/core/implicits.ML b/spartan/core/implicits.ML
deleted file mode 100644
index 2b63f49..0000000
--- a/spartan/core/implicits.ML
+++ /dev/null
@@ -1,87 +0,0 @@
-(*  Title:      implicits.ML
-    Author:     Joshua Chen
-
-Implicit arguments.
-*)
-
-structure Implicits :
-sig
-
-val implicit_defs: Proof.context -> (term * term) Symtab.table
-val implicit_defs_attr: attribute
-val make_holes: Proof.context -> term list -> term list
-
-end = struct
-
-structure Defs = Generic_Data (
-  type T = (term * term) Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  val merge = Symtab.merge (Term.aconv o apply2 #1)
-)
-
-val implicit_defs = Defs.get o Context.Proof
-
-val implicit_defs_attr = Thm.declaration_attribute (fn th =>
-  let
-    val (t, def) = Lib.dest_eq (Thm.prop_of th)
-    val (head, args) = Term.strip_comb t
-    val def' = fold_rev lambda args def
-  in
-    Defs.map (Symtab.update (Term.term_name head, (head, def')))
-  end)
-
-fun make_holes_single ctxt tm name_ctxt =
-  let
-    fun iarg_to_hole (Const (\<^const_name>\<open>iarg\<close>, T)) =
-          Const (\<^const_name>\<open>hole\<close>, T)
-      | iarg_to_hole t = t
-
-    fun expand head args =
-      let fun betapplys (head', args') =
-        Term.betapplys (map_aterms iarg_to_hole head', args')
-      in
-        case head of
-          Abs (x, T, t) =>
-            list_comb (Abs (x, T, Lib.traverse_term expand t), args)
-        | _ =>
-            case Symtab.lookup (implicit_defs ctxt) (Term.term_name head) of
-              SOME (t, def) => betapplys
-                (Envir.expand_atom
-                  (Term.fastype_of head)
-                  (Term.fastype_of t, def),
-                args)
-            | NONE => list_comb (head, args)
-      end
-
-    fun holes_to_vars t =
-      let
-        val count = Lib.subterm_count (Const (\<^const_name>\<open>hole\<close>, dummyT))
-
-        fun subst (Const (\<^const_name>\<open>hole\<close>, T)) (Var (idx, _)::_) Ts =
-              let
-                val bounds = map Bound (0 upto (length Ts - 1))
-                val T' = foldr1 (op -->) (Ts @ [T])
-              in
-                foldl1 (op $) (Var (idx, T')::bounds)
-              end
-          | subst (Abs (x, T, t)) vs Ts = Abs (x, T, subst t vs (T::Ts))
-          | subst (t $ u) vs Ts =
-              let val n = count t
-              in subst t (take n vs) Ts $ subst u (drop n vs) Ts end
-          | subst t _ _ = t
-
-        val names = Name.invent name_ctxt "*" (count t)
-        val vars = map (fn n => Var ((n, 0), dummyT)) names
-      in
-        (subst t vars [], fold Name.declare names name_ctxt)
-      end
-  in
-    holes_to_vars (Lib.traverse_term expand tm)
-  end
-
-fun make_holes ctxt tms = #1
-  (fold_map (make_holes_single ctxt) tms (Variable.names_of ctxt))
-
-
-end
diff --git a/spartan/core/lib.ML b/spartan/core/lib.ML
deleted file mode 100644
index e43ad98..0000000
--- a/spartan/core/lib.ML
+++ /dev/null
@@ -1,193 +0,0 @@
-structure Lib :
-sig
-
-(*Lists*)
-val max: ('a * 'a -> bool) -> 'a list -> 'a
-val maxint: int list -> int
-
-(*Terms*)
-val no_vars: term -> bool
-val is_rigid: term -> bool
-val is_eq: term -> bool
-val dest_prop: term -> term
-val dest_eq: term -> term * term
-val mk_Var: string -> int -> typ -> term
-val lambda_var: term -> term -> term
-
-val is_typing: term -> bool
-val mk_typing: term -> term -> term
-val dest_typing: term -> term * term
-val term_of_typing: term -> term
-val type_of_typing: term -> term
-val mk_Pi: term -> term -> term -> term
-
-val typing_of_term: term -> term
-
-(*Goals*)
-val decompose_goal: Proof.context -> term -> term list * term
-val rigid_typing_concl: term -> bool
-
-(*Theorems*)
-val partition_judgments: thm list -> thm list * thm list * thm list
-
-(*Subterms*)
-val has_subterm: term list -> term -> bool
-val subterm_count: term -> term -> int
-val subterm_count_distinct: term list -> term -> int
-val traverse_term: (term -> term list -> term) -> term -> term
-val collect_subterms: (term -> bool) -> term -> term list
-
-(*Orderings*)
-val subterm_order: term -> term -> order
-val cond_order: order -> order -> order
-
-end = struct
-
-
-(** Lists **)
-
-fun max gt (x::xs) = fold (fn a => fn b => if gt (a, b) then a else b) xs x
-  | max _ [] = error "max of empty list"
-
-val maxint = max (op >)
-
-
-(** Terms **)
-
-(* Meta *)
-
-val no_vars = not o exists_subterm is_Var
-
-val is_rigid = not o is_Var o head_of
-
-fun is_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _) = true
-  | is_eq _ = false
-
-fun dest_prop (Const (\<^const_name>\<open>Pure.prop\<close>, _) $ P) = P
-  | dest_prop P = P
-
-fun dest_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ def) = (t, def)
-  | dest_eq _ = error "dest_eq"
-
-fun mk_Var name idx T = Var ((name, idx), T)
-
-fun lambda_var x tm =
-  let
-    fun var_args (Var (idx, T)) = Var (idx, \<^typ>\<open>o\<close> --> T) $ x
-      | var_args t = t
-  in
-    tm |> map_aterms var_args
-       |> lambda x
-  end
-
-(* Object *)
-
-fun is_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ _ $ _) = true
-  | is_typing _ = false
-
-fun mk_typing t T = \<^const>\<open>has_type\<close> $ t $ T
-
-fun dest_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ t $ T) = (t, T)
-  | dest_typing t = raise TERM ("dest_typing", [t])
-
-val term_of_typing = #1 o dest_typing
-val type_of_typing = #2 o dest_typing
-
-fun mk_Pi v typ body = Const (\<^const_name>\<open>Pi\<close>, dummyT) $ typ $ lambda v body
-
-fun typing_of_term tm = \<^const>\<open>has_type\<close> $ tm $ Var (("*?", 0), \<^typ>\<open>o\<close>)
-(*The above is a bit hacky; basically we need to guarantee that the schematic
-  var is fresh. This works for now because no other code in the Isabelle system
-  or the current logic uses this identifier.*)
-
-
-(** Goals **)
-
-(*Breaks a goal \<And>x ... y. \<lbrakk>P1; ... Pn\<rbrakk> \<Longrightarrow> Q into ([P1, ..., Pn], Q), fixing
-  \<And>-quantified variables and keeping schematics.*)
-fun decompose_goal ctxt goal =
-  let
-    val focus =
-      #1 (Subgoal.focus_prems ctxt 1 NONE (Thm.trivial (Thm.cterm_of ctxt goal)))
-
-    val schematics = #2 (#schematics focus)
-      |> map (fn (v, ctm) => (Thm.term_of ctm, Var v))
-  in
-    map Thm.prop_of (#prems focus) @ [Thm.term_of (#concl focus)]
-    |> map (subst_free schematics)
-    |> (fn xs => chop (length xs - 1) xs) |> apsnd the_single
-  end
-  handle List.Empty => error "Lib.decompose_goal"
-
-fun rigid_typing_concl goal =
-  let val concl = Logic.strip_assums_concl goal
-  in is_typing concl andalso is_rigid (term_of_typing concl) end
-
-
-(** Theorems **)
-fun partition_judgments ths =
-  let
-    fun part [] facts conds eqs = (facts, conds, eqs)
-      | part (th::ths) facts conds eqs =
-          if is_typing (Thm.prop_of th) then
-            part ths (th::facts) conds eqs
-          else if is_typing (Thm.concl_of th) then
-            part ths facts (th::conds) eqs
-          else part ths facts conds (th::eqs)
-  in part ths [] [] [] end
-
-
-(** Subterms **)
-
-fun has_subterm tms =
-  Term.exists_subterm
-    (foldl1 (op orf) (map (fn t => fn s => Term.aconv_untyped (s, t)) tms))
-
-fun subterm_count s t =
-  let
-    fun count (t1 $ t2) i = i + count t1 0 + count t2 0
-      | count (Abs (_, _, t)) i = i + count t 0
-      | count t i = if Term.aconv_untyped (s, t) then i + 1 else i
-  in
-    count t 0
-  end
-
-(*Number of distinct subterms in `tms` that appear in `tm`*)
-fun subterm_count_distinct tms tm =
-  length (filter I (map (fn t => has_subterm [t] tm) tms))
-
-(*
-  "Folds" a function f over the term structure of t by traversing t from child
-  nodes upwards through parents. At each node n in the term syntax tree, f is
-  additionally passed a list of the results of f at all children of n.
-*)
-fun traverse_term f t =
-  let
-    fun map_aux (Abs (x, T, t)) = Abs (x, T, map_aux t)
-      | map_aux t =
-          let
-            val (head, args) = Term.strip_comb t
-            val args' = map map_aux args
-          in
-            f head args'
-          end
-  in
-    map_aux t
-  end
-
-fun collect_subterms f (t $ u) = collect_subterms f t @ collect_subterms f u
-  | collect_subterms f (Abs (_, _, t)) = collect_subterms f t
-  | collect_subterms f t = if f t then [t] else []
-
-
-(** Orderings **)
-
-fun subterm_order t1 t2 =
-  if has_subterm [t1] t2 then LESS
-  else if has_subterm [t2] t1 then GREATER
-  else EQUAL
-
-fun cond_order o1 o2 = case o1 of EQUAL => o2 | _ => o1
-
-
-end
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
deleted file mode 100644
index 923a3a7..0000000
--- a/spartan/core/tactics.ML
+++ /dev/null
@@ -1,180 +0,0 @@
-(*  Title:      tactics.ML
-    Author:     Joshua Chen
-
-General tactics for dependent type theory.
-*)
-
-structure Tactics:
-sig
-
-val solve_side_conds: int Config.T
-val SIDE_CONDS: int -> context_tactic' -> thm list -> context_tactic'
-val rule_ctac: thm list -> context_tactic'
-val dest_ctac: int option -> thm list -> context_tactic'
-val intro_ctac: context_tactic'
-val elim_ctac: term list -> context_tactic'
-val cases_ctac: term -> context_tactic'
-
-end = struct
-
-
-(* Side conditions *)
-val solve_side_conds = Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2)
-
-fun SIDE_CONDS j ctac facts i (cst as (ctxt, st)) = cst |>
-  (case Config.get ctxt solve_side_conds of
-    1 => (ctac CTHEN_ALL_NEW (CTRY o Types.known_ctac facts)) i
-  | 2 => ctac i CTHEN CREPEAT_IN_RANGE (i + j) (Thm.nprems_of st - i)
-      (CTRY o CREPEAT_ALL_NEW_FWD (Types.check_infer facts))
-  | _ => ctac i)
-
-
-(* rule, dest, intro *)
-
-local
-  fun mk_rules _ ths [] = ths
-    | mk_rules n ths ths' =
-        let val ths'' = foldr1 (op @)
-          (map
-            (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => [])
-            ths')
-        in
-          mk_rules n (ths @ ths') ths''
-        end
-in
-
-(*Resolves with given rules*)
-fun rule_ctac ths i (ctxt, st) =
-  TACTIC_CONTEXT ctxt (resolve_tac ctxt (mk_rules 0 [] ths) i st)
-
-(*Attempts destruct-resolution with the n-th premise of the given rules*)
-fun dest_ctac opt_n ths i (ctxt, st) =
-  TACTIC_CONTEXT ctxt (dresolve_tac ctxt
-    (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths)
-    i st)
-
-end
-
-(*Applies an appropriate introduction rule*)
-val intro_ctac = CONTEXT_TACTIC' (fn ctxt => SUBGOAL (fn (goal, i) =>
-  let val concl = Logic.strip_assums_concl goal in
-    if Lib.is_typing concl andalso Lib.is_rigid (Lib.type_of_typing concl)
-    then resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) i
-    else no_tac
-  end))
-
-
-(* Induction/elimination *)
-
-(*Pushes a known typing t:T into a \<Prod>-type.
-  This tactic is well-behaved only when t is sufficiently well specified
-  (otherwise there might be multiple possible judgments t:T that unify, and
-  which is chosen is undefined).*)
-fun internalize_fact_tac t =
-  Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl = raw_concl, ...} =>
-    let
-      val concl = Logic.strip_assums_concl (Thm.term_of raw_concl)
-      val C = Lib.type_of_typing concl
-      val B = Thm.cterm_of ctxt (Lib.lambda_var t C)
-      val a = Thm.cterm_of ctxt t
-      (*The resolvent is PiE[where ?B=B and ?a=a]*)
-      val resolvent =
-        Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
-    in
-      HEADGOAL (resolve_tac ctxt [resolvent])
-      (*Unify with the correct type T*)
-      THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.known_ctac [])
-    end)
-
-fun elim_core_tac tms types ctxt =
-  let
-    val rule_insts = map ((Elim.lookup_rule ctxt) o Term.head_of) types
-    val rules = flat (map
-      (fn rule_inst => case rule_inst of
-          NONE => []
-        | SOME (rl, idxnames) => [Drule.infer_instantiate ctxt
-          (idxnames ~~ map (Thm.cterm_of ctxt) tms) rl])
-      rule_insts)
-  in
-    resolve_tac ctxt rules
-    THEN' RANGE (replicate (length tms) (NO_CONTEXT_TACTIC ctxt o Types.check_infer []))
-  end handle Option => K no_tac
-
-(*Premises that have already been pushed into the \<Prod>-type*)
-structure Inserts = Proof_Data (
-  type T = term Item_Net.T
-  val init = K (Item_Net.init Term.aconv_untyped single)
-)
-
-fun elim_ctac tms =
-  case tms of
-    [] => CONTEXT_TACTIC' (fn ctxt => eresolve_tac ctxt (map #1 (Elim.rules ctxt)))
-  | major :: _ => CONTEXT_SUBGOAL (fn (goal, _) => fn cst as (ctxt, st) =>
-      let
-        val facts = map Thm.prop_of (Context_Facts.known ctxt)
-        val prems = Logic.strip_assums_hyp goal
-        val template = Lib.typing_of_term major
-        val types = filter (fn th => Term.could_unify (template, th)) (facts @ prems)
-          |> map Lib.type_of_typing
-      in case types of
-          [] => no_ctac cst
-        | _ =>
-            let
-              val inserts = facts @ prems
-                |> filter Lib.is_typing
-                |> map Lib.dest_typing
-                |> filter_out (fn (t, _) =>
-                  Term.aconv (t, major) orelse Item_Net.member (Inserts.get ctxt) t)
-                |> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct tms T))
-                |> filter (fn (_, i) => i > 0)
-                (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
-                  If they are incomparable, then order by decreasing
-                  `subterm_count [p, x, y] T`*)
-                |> sort (fn (((t1, _), i), ((_, T2), j)) =>
-                    Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
-                |> map (#1 o #1)
-              val record_inserts = Inserts.map (fold Item_Net.update inserts)
-              val tac =
-                (*Push premises having a subterm in `tms` into a \<Prod>*)
-                fold (fn t => fn tac =>
-                  tac THEN HEADGOAL (internalize_fact_tac t ctxt))
-                  inserts all_tac
-                (*Apply elimination rule*)
-                THEN HEADGOAL (
-                  elim_core_tac tms types ctxt
-                  (*Pull pushed premises back out*)
-                  THEN_ALL_NEW (SUBGOAL (fn (_, i) =>
-                    REPEAT_DETERM_N (length inserts)
-                      (resolve_tac ctxt @{thms PiI[rotated]} i))))
-            in
-              TACTIC_CONTEXT (record_inserts ctxt) (tac st)
-            end
-      end)
-
-fun cases_ctac tm =
-  let fun tac ctxt =
-    SUBGOAL (fn (goal, i) =>
-      let
-        val facts = Proof_Context.facts_of ctxt
-        val prems = Logic.strip_assums_hyp goal
-        val template = Lib.typing_of_term tm
-        val types =
-          map (Thm.prop_of o #1) (Facts.could_unify facts template)
-          @ filter (fn prem => Term.could_unify (template, prem)) prems
-          |> map Lib.type_of_typing
-        val res = (case types of
-            [typ] => Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt tm)]
-              (the (Case.lookup_rule ctxt (Term.head_of typ)))
-          | [] => raise Option
-          | _ => raise error (Syntax.string_of_term ctxt tm ^ "not uniquely typed"))
-          handle Option =>
-            error ("No case rule known for " ^ (Syntax.string_of_term ctxt tm))
-      in
-        resolve_tac ctxt [res] i
-      end)
-  in CONTEXT_TACTIC' tac end
-
-
-end
-
-open Tactics
diff --git a/spartan/core/types.ML b/spartan/core/types.ML
deleted file mode 100644
index 5e0d484..0000000
--- a/spartan/core/types.ML
+++ /dev/null
@@ -1,113 +0,0 @@
-(*  Title:      types.ML
-    Author:     Joshua Chen
-
-Type-checking infrastructure.
-*)
-
-structure Types: sig
-
-val debug_typechk: bool Config.T
-
-val known_ctac: thm list -> int -> context_tactic
-val check_infer: thm list -> int -> context_tactic
-
-end = struct
-
-open Context_Facts
-
-(** [type] attribute **)
-
-val _ = Theory.setup (
-  Attrib.setup \<^binding>\<open>type\<close>
-    (Scan.succeed (Thm.declaration_attribute (fn th =>
-      if Thm.no_prems th then register_known th else register_cond th)))
-    ""
-  #> Global_Theory.add_thms_dynamic (\<^binding>\<open>type\<close>,
-      fn context => let val ctxt = Context.proof_of context in
-        known ctxt @ cond ctxt end)
-)
-
-
-(** Context tactics for type-checking and elaboration **)
-
-val debug_typechk = Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
-
-fun debug_tac ctxt s =
-  if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac
-
-(*Solves goals without metavariables and type inference problems by assumption
-  from inline premises or resolution with facts*)
-fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
-  TACTIC_CONTEXT ctxt
-    let val concl = Logic.strip_assums_concl goal in
-      if Lib.no_vars concl orelse
-        (Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl))
-      then
-        let val ths = known ctxt @ facts
-        in st |>
-          (assume_tac ctxt ORELSE' resolve_tac ctxt ths THEN_ALL_NEW K no_tac) i
-        end
-      else Seq.empty
-    end)
-
-(*Simple bidirectional typing tactic with some backtracking search over input
-  facts.*)
-fun check_infer_step facts i (ctxt, st) =
-  let
-    val refine_tac = SUBGOAL (fn (goal, i) =>
-      if Lib.rigid_typing_concl goal
-      then
-        let
-          val net = Tactic.build_net (
-            map (Simplifier.norm_hhf ctxt) facts
-            @(cond ctxt)
-            @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
-            @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
-            @(map #1 (Elim.rules ctxt)))
-        in resolve_from_net_tac ctxt net i end
-      else no_tac)
-
-    val sub_tac = SUBGOAL (fn (goal, i) =>
-      let val concl = Logic.strip_assums_concl goal in
-      if Lib.is_typing concl
-        andalso Lib.is_rigid (Lib.term_of_typing concl)
-        andalso Lib.no_vars (Lib.type_of_typing concl)
-      then
-        (resolve_tac ctxt @{thms sub}
-        THEN' SUBGOAL (fn (_, i) =>
-          NO_CONTEXT_TACTIC ctxt (check_infer facts i))
-        THEN' compute_tac ctxt facts
-        THEN_ALL_NEW K no_tac) i
-      else no_tac end)
-
-    val ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*)
-  in
-    TACTIC_CONTEXT ctxt' (
-      (NO_CONTEXT_TACTIC ctxt' o known_ctac facts
-      ORELSE' refine_tac
-      ORELSE' sub_tac) i st)
-  end
-
-and check_infer facts i (cst as (_, st)) =
-  let
-    val ctac = check_infer_step facts
-  in
-    cst |> (ctac i CTHEN
-      CREPEAT_IN_RANGE i (Thm.nprems_of st - i) (CTRY o CREPEAT_ALL_NEW_FWD ctac))
-  end
-
-and compute_tac ctxt facts =
-  let
-    val comps = Named_Theorems.get ctxt \<^named_theorems>\<open>comp\<close>
-    val ss = simpset_of ctxt
-    val ss' = simpset_of (empty_simpset ctxt addsimps comps)
-    val ctxt' = put_simpset (merge_ss (ss, ss')) ctxt
-  in
-    SUBGOAL (fn (_, i) =>
-      ((CHANGED o asm_simp_tac ctxt' ORELSE' EqSubst.eqsubst_tac ctxt [0] comps)
-      THEN_ALL_NEW SUBGOAL (fn (_, i) =>
-        NO_CONTEXT_TACTIC ctxt (check_infer facts i))) i)
-  end
-
-
-end