diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
index 26eda236c..3e9784c07 100644
--- a/src/builtin/CMakeLists.txt
+++ b/src/builtin/CMakeLists.txt
@@ -54,7 +54,7 @@ function(add_kernel_theory FILE)
   if(CMAKE_CROSSCOMPILING)
     copy_olean(${FILE})
   else()
-    add_theory_core(${FILE} "-k" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua")
+    add_theory_core(${FILE} "-n" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua")
   endif()
 endfunction()
 
@@ -62,13 +62,13 @@ function(add_theory FILE)
   if(CMAKE_CROSSCOMPILING)
     copy_olean(${FILE})
   else()
-    add_theory_core(${FILE} "" "${CMAKE_CURRENT_BINARY_DIR}/basic.olean")
+    add_theory_core(${FILE} "" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
   endif()
 endfunction()
 
-add_kernel_theory("basic.lean")
+add_kernel_theory("kernel.lean")
 add_kernel_theory("nat.lean")
-add_dependencies(nat_builtin basic_builtin)
+add_dependencies(nat_builtin kernel_builtin)
 add_kernel_theory("int.lean")
 add_dependencies(int_builtin nat_builtin)
 add_kernel_theory("real.lean")
@@ -77,6 +77,7 @@ add_kernel_theory("specialfn.lean")
 add_dependencies(specialfn_builtin real_builtin)
 add_theory("cast.lean")
 # TODO(Leo): Remove the following dependencies after cleanup
+add_dependencies(cast_builtin kernel_builtin)
 add_dependencies(cast_builtin nat_builtin)
 add_dependencies(cast_builtin int_builtin)
 add_dependencies(cast_builtin real_builtin)
diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean
index 59c5f21fc..481d07bb3 100644
Binary files a/src/builtin/cast.olean and b/src/builtin/cast.olean differ
diff --git a/src/builtin/int.lean b/src/builtin/int.lean
index 31d925bb7..72e81e81c 100644
--- a/src/builtin/int.lean
+++ b/src/builtin/int.lean
@@ -1,4 +1,3 @@
-Import basic.
 Import nat.
 
 Variable Int : Type.
diff --git a/src/builtin/int.olean b/src/builtin/int.olean
index cf813ba93..e5a503925 100644
Binary files a/src/builtin/int.olean and b/src/builtin/int.olean differ
diff --git a/src/builtin/basic.lean b/src/builtin/kernel.lean
similarity index 100%
rename from src/builtin/basic.lean
rename to src/builtin/kernel.lean
diff --git a/src/builtin/basic.olean b/src/builtin/kernel.olean
similarity index 100%
rename from src/builtin/basic.olean
rename to src/builtin/kernel.olean
diff --git a/src/builtin/nat.lean b/src/builtin/nat.lean
index efaf7bef7..e72e34c01 100644
--- a/src/builtin/nat.lean
+++ b/src/builtin/nat.lean
@@ -1,4 +1,4 @@
-Import basic.
+Import kernel.
 
 Variable Nat : Type.
 Alias ℕ : Nat.
diff --git a/src/builtin/nat.olean b/src/builtin/nat.olean
index 398e51d73..445ede6f4 100644
Binary files a/src/builtin/nat.olean and b/src/builtin/nat.olean differ
diff --git a/src/builtin/real.lean b/src/builtin/real.lean
index 63b606d09..700fde539 100644
--- a/src/builtin/real.lean
+++ b/src/builtin/real.lean
@@ -1,5 +1,3 @@
-Import basic.
-Import nat.
 Import int.
 
 Variable Real : Type.
diff --git a/src/builtin/real.olean b/src/builtin/real.olean
index 5e94086d5..6ae12d3c8 100644
Binary files a/src/builtin/real.olean and b/src/builtin/real.olean differ
diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 29822687c..3b968c40e 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -557,9 +557,9 @@ static lean_extension & to_ext(environment const & env) {
 /**
    \brief Import all definitions and notation.
 */
-void init_frontend(environment const & env, io_state & ios, bool kernel_only) {
+void init_frontend(environment const & env, io_state & ios, bool no_kernel) {
     ios.set_formatter(mk_pp_formatter(env));
-    if (!kernel_only)
+    if (!no_kernel)
         import_all(env);
 }
 void init_frontend(environment const & env) {
diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h
index 77037e71b..9d73d22c0 100644
--- a/src/frontends/lean/frontend.h
+++ b/src/frontends/lean/frontend.h
@@ -16,7 +16,7 @@ namespace lean {
 /**
    \brief Import all definitions and notation.
 */
-void init_frontend(environment const & env, io_state & ios, bool kernel_only = false);
+void init_frontend(environment const & env, io_state & ios, bool no_kernel = false);
 void init_frontend(environment const & env);
 
 /**
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index f76826dd7..f8fd08084 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -7,10 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
-
-#ifndef LEAN_DEFAULT_LEVEL_SEPARATION
-#define LEAN_DEFAULT_LEVEL_SEPARATION 512
-#endif
+#include "kernel/io_state.h"
 
 namespace lean {
 // =======================================
@@ -139,7 +136,44 @@ MK_CONSTANT(subst_fn,       name("Subst"));
 MK_CONSTANT(eta_fn,         name("Eta"));
 MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 MK_CONSTANT(abst_fn,        name("Abst"));
-
 MK_CONSTANT(htrans_fn,      name("HTrans"));
 MK_CONSTANT(hsymm_fn,       name("HSymm"));
+// Theorems
+MK_CONSTANT(trivial,            name("Trivial"));
+MK_CONSTANT(true_neq_false,     name("TrueNeFalse"));
+MK_CONSTANT(false_elim_fn,      name("FalseElim"));
+MK_CONSTANT(absurd_fn,          name("Absurd"));
+MK_CONSTANT(em_fn,              name("EM"));
+MK_CONSTANT(double_neg_fn,      name("DoubleNeg"));
+MK_CONSTANT(double_neg_elim_fn, name("DoubleNegElim"));
+MK_CONSTANT(mt_fn,              name("MT"));
+MK_CONSTANT(contrapos_fn,       name("Contrapos"));
+MK_CONSTANT(false_imp_any_fn,   name("FalseImpAny"));
+MK_CONSTANT(absurd_elim_fn,     name("AbsurdElim"));
+MK_CONSTANT(eq_mp_fn,           name("EqMP"));
+MK_CONSTANT(not_imp1_fn,        name("NotImp1"));
+MK_CONSTANT(not_imp2_fn,        name("NotImp2"));
+MK_CONSTANT(conj_fn,            name("Conj"));
+MK_CONSTANT(conjunct1_fn,       name("Conjunct1"));
+MK_CONSTANT(conjunct2_fn,       name("Conjunct2"));
+MK_CONSTANT(disj1_fn,           name("Disj1"));
+MK_CONSTANT(disj2_fn,           name("Disj2"));
+MK_CONSTANT(disj_cases_fn,      name("DisjCases"));
+MK_CONSTANT(refute_fn,          name("Refute"));
+MK_CONSTANT(symm_fn,            name("Symm"));
+MK_CONSTANT(trans_fn,           name("Trans"));
+MK_CONSTANT(congr1_fn,          name("Congr1"));
+MK_CONSTANT(congr2_fn,          name("Congr2"));
+MK_CONSTANT(congr_fn,           name("Congr"));
+MK_CONSTANT(eqt_elim_fn,        name("EqTElim"));
+MK_CONSTANT(eqt_intro_fn,       name("EqTIntro"));
+MK_CONSTANT(forall_elim_fn,     name("ForallElim"));
+MK_CONSTANT(forall_intro_fn,    name("ForallIntro"));
+MK_CONSTANT(exists_elim_fn,     name("ExistsElim"));
+MK_CONSTANT(exists_intro_fn,    name("ExistsIntro"));
+
+void import_kernel(environment const & env) {
+    io_state ios;
+    env->import("kernel", ios);
+}
 }
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 3bbe713af..8410315c4 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -8,10 +8,8 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-/** \brief Return (Type m)  m >= bottom + Offset */
+// See src/builtin/kernel.lean for signatures.
 extern expr const TypeM;
-
-/** \brief Return (Type u)  u >= m + Offset */
 extern expr const TypeU;
 
 /** \brief Return the Lean Boolean type. */
@@ -35,135 +33,192 @@ bool is_true(expr const & e);
 /** \brief Return true iff \c e is the Lean false value. */
 bool is_false(expr const & e);
 
-/** \brief Return the Lean If-Then-Else operator. It has type: pi (A : Type), bool -> A -> A -> A */
 expr mk_if_fn();
 bool is_if_fn(expr const & e);
 inline bool is_if(expr const & e) { return is_app(e) && is_if_fn(arg(e, 0)); }
-/** \brief Return the term (if A c t e) */
 inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); }
 inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); }
-/** \brief Return the term (if bool c t e) */
 inline expr mk_bool_if(expr const & c, expr const & t, expr const & e) { return mk_if(mk_bool_type(), c, t, e); }
 inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool_if(c, t, e); }
 
-/** \brief Return the Lean Implies operator */
 expr mk_implies_fn();
 bool is_implies_fn(expr const & e);
 inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
-/** \brief Return the term (e1 => e2) */
 inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); }
 inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
 
-/** \brief Return the Lean Iff operator */
 expr mk_iff_fn();
 bool is_iff_fn(expr const & e);
 inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); }
-/** \brief Return (e1 iff e2) */
 inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); }
 inline expr Iff(expr const & e1, expr const & e2) { return mk_iff(e1, e2); }
 
-/** \brief Return the Lean And operator */
 expr mk_and_fn();
 bool is_and_fn(expr const & e);
 inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
-/** \brief Return (e1 and e2) */
 inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); }
 inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
 
-/** \brief Return the Lean Or operator */
 expr mk_or_fn();
 bool is_or_fn(expr const & e);
 inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); }
-/** \brief Return (e1 Or e2) */
 inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); }
 inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); }
 
-/** \brief Return the Lean not operator */
 expr mk_not_fn();
 bool is_not_fn(expr const & e);
 inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
-/** \brief Return (Not e) */
 inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); }
 inline expr Not(expr const & e) { return mk_not(e); }
 
-/** \brief Return the Lean forall operator. It has type: <tt>Pi (A : Type), (A -> bool) -> Bool</tt> */
 expr mk_forall_fn();
 bool is_forall_fn(expr const & e);
 inline bool is_forall(expr const & e) { return is_app(e) && is_forall_fn(arg(e, 0)); }
-/** \brief Return the term (Forall A P), where A is a type and P : A -> bool */
 inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); }
 inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); }
 
-/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool</tt> */
 expr mk_exists_fn();
 bool is_exists_fn(expr const & e);
 inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); }
-/** \brief Return the term (exists A P), where A is a type and P : A -> bool */
 inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
 inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
 
-/** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool</tt> */
 expr mk_homo_eq_fn();
 bool is_homo_eq_fn(expr const & e);
 inline bool is_homo_eq(expr const & e) { return is_app(e) && is_homo_eq_fn(arg(e, 0)); }
-/** \brief Return the term (homo_eq A l r) */
 inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
 inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }
 
-/** \brief Modus Ponens axiom */
 expr mk_mp_fn();
-/** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */
 inline expr MP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mp_fn(), a, b, H1, H2); }
 
-/** \brief Discharge axiom */
 expr mk_discharge_fn();
-/** \brief (Axiom) {a : Bool}, {b : Bool}, H : a -> b |- Discharge(a, b, H) : a => b */
 inline expr Discharge(expr const & a, expr const & b, expr const & H) { return mk_app(mk_discharge_fn(), a, b, H); }
 
-/** \brief Case analysis axiom */
 expr mk_case_fn();
-/** \brief (Axiom) P : Bool -> Bool, H1 : P True, H2 : P False, a : Bool |- Case(P, H1, H2, a) : P a */
 inline expr Case(expr const & P, expr const & H1, expr const & H2, expr const & a) { return mk_app(mk_case_fn(), P, H1, H2, a); }
 
-/** \brief Reflexivity axiom */
 expr mk_refl_fn();
-/** \brief (Axiom) {A : Type u}, a : A |- Refl(A, a) : a = a */
 inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); }
 
-/** \brief Substitution axiom */
 expr mk_subst_fn();
-/** \brief (Axiom) {A : Type u}, {a b : A}, P : A -> Bool, H1 : P a, H2 : a = b |- Subst(A, a, b, P, H1, H2) : P b */
 inline expr Subst(expr const & A, expr const & a, expr const & b, expr const & P, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, a, b, P, H1, H2}); }
 
-/** \brief Eta conversion axiom */
 expr mk_eta_fn();
-/** \brief (Axiom) {A : Type u}, {B : A -> Type u}, f : (Pi x : A, B x) |- Eta(A, B, f) : ((Fun x : A => f x) = f) */
 inline expr Eta(expr const & A, expr const & B, expr const & f) { return mk_app(mk_eta_fn(), A, B, f); }
 
-/** \brief Implies Anti-symmetry */
 expr mk_imp_antisym_fn();
-/** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
 inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
 
-/** \brief Abstraction axiom */
 expr mk_abst_fn();
-/** \brief (Axiom) {A : Type u} {B : A -> Type u}, f g : {Pi x : A, B x}, H : (Pi x : A, (f x) = (g x)) |- Abst(A, B, f, g, H) : f = g */
 inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, expr const & H) { return mk_app({mk_abst_fn(), A, B, f, g, H}); }
 
-/** \brief Heterogeneous symmetry axiom */
 expr mk_hsymm_fn();
-/** \brief (Axiom) {A : Type u}, {B : Type u}, {a : A}, {b : B}, H1 : a = b |- HSymm(A, B, a, b, H1) : b = a */
-inline expr HSymm(expr const & A, expr const & B, expr const & a, expr const & b, expr const & H1) {
-    return mk_app({mk_hsymm_fn(), A, B, a, b, H1});
-}
+inline expr HSymm(expr const & A, expr const & B, expr const & a, expr const & b, expr const & H1) { return mk_app({mk_hsymm_fn(), A, B, a, b, H1}); }
 
-/** \brief Heterogeneous Transitivity axiom */
 expr mk_htrans_fn();
-/** \brief (Axiom) {A : Type u}, {B : Type u}, {C : Type u}, {a : A}, {b : B} {c : C}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
 inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) {
     return mk_app({mk_htrans_fn(), A, B, C, a, b, c, H1, H2});
 }
 
+expr mk_trivial();
+#define Trivial mk_trivial()
+
+expr mk_true_ne_false();
+#define TrueNeFalse mk_true_ne_false();
+
+expr mk_em_fn();
+inline expr EM(expr const & a) { return mk_app(mk_em_fn(), a); }
+
+expr mk_false_elim_fn();
+inline expr FalseElim(expr const & a, expr const & H) { return mk_app(mk_false_elim_fn(), a, H); }
+
+expr mk_absurd_fn();
+inline expr Absurd(expr const & a, expr const & H1, expr const & H2) { return mk_app(mk_absurd_fn(), a, H1, H2); }
+
+expr mk_double_neg_fn();
+inline expr DoubleNeg(expr const & a) { return mk_app(mk_double_neg_fn(), a); }
+
+expr mk_double_neg_elim_fn();
+inline expr DoubleNegElim(expr const & P, expr const & H) { return mk_app(mk_double_neg_elim_fn(), P, H); }
+
+expr mk_mt_fn();
+inline expr MT(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mt_fn(), a, b, H1, H2); }
+
+expr mk_contrapos_fn();
+inline expr Contrapos(expr const & a, expr const & b, expr const & H) { return mk_app(mk_contrapos_fn(), a, b, H); }
+
+expr mk_false_imp_any_fn();
+inline expr FalseImpAny(expr const & a) { return mk_app(mk_false_imp_any_fn(), a); }
+
+expr mk_absurd_elim_fn();
+inline expr AbsurdElim(expr const & a, expr const & c, expr const & H1, expr const & H2) {
+    return mk_app(mk_absurd_elim_fn(), a, c, H1, H2);
+}
+
+expr mk_eq_mp_fn();
+inline expr EqMP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_eq_mp_fn(), a, b, H1, H2); }
+
+expr mk_not_imp1_fn();
+inline expr NotImp1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp1_fn(), a, b, H); }
+
+expr mk_not_imp2_fn();
+inline expr NotImp2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp2_fn(), a, b, H); }
+
+expr mk_conj_fn();
+inline expr Conj(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_conj_fn(), a, b, H1, H2); }
+
+expr mk_conjunct1_fn();
+inline expr Conjunct1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct1_fn(), a, b, H); }
+
+expr mk_conjunct2_fn();
+inline expr Conjunct2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct2_fn(), a, b, H); }
+
+expr mk_disj1_fn();
+inline expr Disj1(expr const & a, expr const & H, expr const & b) { return mk_app(mk_disj1_fn(), a, H, b); }
+
+expr mk_disj2_fn();
+inline expr Disj2(expr const & b, expr const & a, expr const & H) { return mk_app(mk_disj2_fn(), b, a, H); }
+
+expr mk_disj_cases_fn();
+inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); }
+
+expr mk_refute_fn();
+inline expr Refute(expr const & a, expr const & H) { return mk_app({mk_refute_fn(), a, H}); }
+
+expr mk_symm_fn();
+inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); }
+
+expr mk_trans_fn();
+inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); }
+
+expr mk_eqt_elim_fn();
+inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }
+
+expr mk_eqt_intro_fn();
+inline expr EqTIntro(expr const & a, expr const & H) { return mk_app(mk_eqt_intro_fn(), a, H); }
+
+expr mk_congr1_fn();
+inline expr Congr1(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & H) { return mk_app({mk_congr1_fn(), A, B, f, g, a, H}); }
+
+expr mk_congr2_fn();
+inline expr Congr2(expr const & A, expr const & B, expr const & a, expr const & b, expr const & f, expr const & H) { return mk_app({mk_congr2_fn(), A, B, a, b, f, H}); }
+
+expr mk_congr_fn();
+inline expr Congr(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_congr_fn(), A, B, f, g, a, b, H1, H2}); }
+
+expr mk_forall_elim_fn();
+inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); }
+
+expr mk_forall_intro_fn();
+inline expr ForallIntro(expr const & A, expr const & P, expr const & H) { return mk_app(mk_forall_intro_fn(), A, P, H); }
+
+expr mk_exists_elim_fn();
+inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr const & H1, expr const & H2) { return mk_app({mk_exists_elim_fn(), A, P, B, H1, H2}); }
+
+expr mk_exists_intro_fn();
+inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); }
+
 /**
    \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
 */
@@ -191,4 +246,6 @@ bool Name(expr const & e) {                                             \
     expr const & v = Builtin;                                           \
     return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \
 }
+
+void import_kernel(environment const & env);
 }
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 32d6d96e1..66fb0e063 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,5 +1,5 @@
-add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp
-  max_sharing.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp
-  substitution.cpp fo_unify.cpp bin_op.cpp)
+add_library(library kernel_bindings.cpp deep_copy.cpp max_sharing.cpp
+  context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
+  fo_unify.cpp bin_op.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/all/all.cpp b/src/library/all/all.cpp
index 4536ddc36..01056cf32 100644
--- a/src/library/all/all.cpp
+++ b/src/library/all/all.cpp
@@ -5,13 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/builtin.h"
-#include "library/basic_thms.h"
 #include "library/arith/arith.h"
 #include "library/all/all.h"
 
 namespace lean {
 void import_all(environment const & env) {
-    import_basic_thms(env);
+    import_kernel(env);
     import_arith(env);
 }
 environment mk_toplevel() {
diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp
deleted file mode 100644
index 4d0886473..000000000
--- a/src/library/basic_thms.cpp
+++ /dev/null
@@ -1,50 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/environment.h"
-#include "kernel/io_state.h"
-#include "library/basic_thms.h"
-
-namespace lean {
-
-MK_CONSTANT(trivial,            name("Trivial"));
-MK_CONSTANT(true_neq_false,     name("TrueNeFalse"));
-MK_CONSTANT(false_elim_fn,      name("FalseElim"));
-MK_CONSTANT(absurd_fn,          name("Absurd"));
-MK_CONSTANT(em_fn,              name("EM"));
-MK_CONSTANT(double_neg_fn,      name("DoubleNeg"));
-MK_CONSTANT(double_neg_elim_fn, name("DoubleNegElim"));
-MK_CONSTANT(mt_fn,              name("MT"));
-MK_CONSTANT(contrapos_fn,       name("Contrapos"));
-MK_CONSTANT(false_imp_any_fn,   name("FalseImpAny"));
-MK_CONSTANT(absurd_elim_fn,     name("AbsurdElim"));
-MK_CONSTANT(eq_mp_fn,           name("EqMP"));
-MK_CONSTANT(not_imp1_fn,        name("NotImp1"));
-MK_CONSTANT(not_imp2_fn,        name("NotImp2"));
-MK_CONSTANT(conj_fn,            name("Conj"));
-MK_CONSTANT(conjunct1_fn,       name("Conjunct1"));
-MK_CONSTANT(conjunct2_fn,       name("Conjunct2"));
-MK_CONSTANT(disj1_fn,           name("Disj1"));
-MK_CONSTANT(disj2_fn,           name("Disj2"));
-MK_CONSTANT(disj_cases_fn,      name("DisjCases"));
-MK_CONSTANT(refute_fn,          name("Refute"));
-MK_CONSTANT(symm_fn,            name("Symm"));
-MK_CONSTANT(trans_fn,           name("Trans"));
-MK_CONSTANT(congr1_fn,          name("Congr1"));
-MK_CONSTANT(congr2_fn,          name("Congr2"));
-MK_CONSTANT(congr_fn,           name("Congr"));
-MK_CONSTANT(eqt_elim_fn,        name("EqTElim"));
-MK_CONSTANT(eqt_intro_fn,       name("EqTIntro"));
-MK_CONSTANT(forall_elim_fn,     name("ForallElim"));
-MK_CONSTANT(forall_intro_fn,    name("ForallIntro"));
-MK_CONSTANT(exists_elim_fn,     name("ExistsElim"));
-MK_CONSTANT(exists_intro_fn,    name("ExistsIntro"));
-
-void import_basic_thms(environment const & env) {
-    io_state ios;
-    env->import("basic", ios);
-}
-}
diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h
deleted file mode 100644
index 8195ff513..000000000
--- a/src/library/basic_thms.h
+++ /dev/null
@@ -1,143 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/builtin.h"
-
-namespace lean {
-expr mk_trivial();
-/** \brief (Theorem) Trivial : True */
-#define Trivial mk_trivial()
-
-expr mk_true_ne_false();
-/** \brief (Theorem) TrueNeFalse : Not(True = False) */
-#define TrueNeFalse mk_true_ne_false();
-
-expr mk_em_fn();
-/** \brief (Theorem) a : Bool |- EM(a) : Or(a, Not(a)) */
-inline expr EM(expr const & a) { return mk_app(mk_em_fn(), a); }
-
-expr mk_false_elim_fn();
-/** \brief (Theorem) a : Bool, H : False |- FalseElim(a, H) : a */
-inline expr FalseElim(expr const & a, expr const & H) { return mk_app(mk_false_elim_fn(), a, H); }
-
-expr mk_absurd_fn();
-/** \brief (Theorem) {a : Bool}, H1 : a, H2 : Not(a) |- Absurd(a, H1, H2) : False */
-inline expr Absurd(expr const & a, expr const & H1, expr const & H2) { return mk_app(mk_absurd_fn(), a, H1, H2); }
-
-expr mk_double_neg_fn();
-/** \brief (Theorem) a : Bool |- DoubleNeg(a) : Neg(Neg(a)) = a */
-inline expr DoubleNeg(expr const & a) { return mk_app(mk_double_neg_fn(), a); }
-
-expr mk_double_neg_elim_fn();
-/** \brief (Theorem) {P : Bool}, H : Not (Not P) |- DoubleNegElim(P, H) : P */
-inline expr DoubleNegElim(expr const & P, expr const & H) { return mk_app(mk_double_neg_elim_fn(), P, H); }
-
-expr mk_mt_fn();
-/** \brief (Theorem) {a b : Bool}, H1 : a => b, H2 : Not(b) |- MT(a, b, H1, H2) : Not(a) */
-inline expr MT(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mt_fn(), a, b, H1, H2); }
-
-expr mk_contrapos_fn();
-/** \brief (Theorem) {a b : Bool}, H : a => b |- Contrapos(a, b, H): Neg(b) => Neg(a) */
-inline expr Contrapos(expr const & a, expr const & b, expr const & H) { return mk_app(mk_contrapos_fn(), a, b, H); }
-
-expr mk_false_imp_any_fn();
-/** \brief (Theorem) a : Bool |- false => a */
-inline expr FalseImpAny(expr const & a) { return mk_app(mk_false_imp_any_fn(), a); }
-
-expr mk_absurd_elim_fn();
-/** \brief (Theorem) {a c : Bool}, H1 : a, H2 : Not(a) |- AbsurdImpAny(a, H1, H2) : c */
-inline expr AbsurdElim(expr const & a, expr const & c, expr const & H1, expr const & H2) {
-    return mk_app(mk_absurd_elim_fn(), a, c, H1, H2);
-}
-
-expr mk_eq_mp_fn();
-/** \brief (Theorem) {a b : Bool}, H1 : a = b, H2 : a |- EqMP(a, b, H1, H2) : b */
-inline expr EqMP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_eq_mp_fn(), a, b, H1, H2); }
-
-expr mk_not_imp1_fn();
-/** \brief (Theorem) {a b : Bool}, H : Not(Implies(a, b)) |- NotImp1(a, b, H) : a */
-inline expr NotImp1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp1_fn(), a, b, H); }
-
-expr mk_not_imp2_fn();
-/** \brief (Theorem) {a b : Bool}, H : Not(Implies(a, b)) |- NotImp2(a, b, H) : Not(b) */
-inline expr NotImp2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp2_fn(), a, b, H); }
-
-expr mk_conj_fn();
-/** \brief (Theorem) {a b : Bool}, H1 : a, H2 : b |- Conj(a, b, H1, H2) : And(a, b) */
-inline expr Conj(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_conj_fn(), a, b, H1, H2); }
-
-expr mk_conjunct1_fn();
-/** \brief (Theorem) {a b : Bool}, H : And(a, b) |- Conjunct1(a, b, H) : a */
-inline expr Conjunct1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct1_fn(), a, b, H); }
-
-expr mk_conjunct2_fn();
-/** \brief (Theorem) {a b : Bool}, H : And(a, b) |- Conjunct2(a, b, H) : b */
-inline expr Conjunct2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct2_fn(), a, b, H); }
-
-expr mk_disj1_fn();
-/** \brief (Theorem) a : Bool, H : a, b : Bool |- Disj1(a, H, b) : Or(a, b) */
-inline expr Disj1(expr const & a, expr const & H, expr const & b) { return mk_app(mk_disj1_fn(), a, H, b); }
-
-expr mk_disj2_fn();
-/** \brief (Theorem) {b} a : Bool, H : b |- Disj2(a, b, H) : Or(a, b) */
-inline expr Disj2(expr const & b, expr const & a, expr const & H) { return mk_app(mk_disj2_fn(), b, a, H); }
-
-expr mk_disj_cases_fn();
-/** \brief (Theorem) {a b c : Bool}, H1 : Or(a, b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */
-inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); }
-
-expr mk_refute_fn();
-/** \brief (Theorem) {a : Bool} (H : not a -> false) |- Refute(a, H) : a */
-inline expr Refute(expr const & a, expr const & H) { return mk_app({mk_refute_fn(), a, H}); }
-
-expr mk_symm_fn();
-/** \brief (Theorem) {A : Type u}, {a b : A}, H : a = b |- Symm(A, a, b, H) : b = a */
-inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); }
-
-expr mk_trans_fn();
-/** \brief (Theorem) {A : Type u}, {a b c : A}, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */
-inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); }
-
-expr mk_eqt_elim_fn();
-/** \brief (Theorem) {a : Bool}, H : a = True |- EqTElim(a, H) : a */
-inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }
-
-expr mk_eqt_intro_fn();
-/** \brief (Theorem) {a : Bool}, H : a |- EqTIntro(a, H) : a = True */
-inline expr EqTIntro(expr const & a, expr const & H) { return mk_app(mk_eqt_intro_fn(), a, H); }
-
-expr mk_congr1_fn();
-/** \brief (Theorem) {A : Type u}, {B : A -> Type u}, {f g : (Pi x : A, B x)}, a : A, H : f = g |- Congr2(A, B, f, g, a, H) : f a = g a */
-inline expr Congr1(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & H) { return mk_app({mk_congr1_fn(), A, B, f, g, a, H}); }
-
-expr mk_congr2_fn();
-/** \brief (Theorem) {A : Type u}, {B : A -> Type u}, {a b : A}, f : (Pi x : A, B x), H : a = b |- Congr1(A, B, f, a, b, H) : f a = f b */
-inline expr Congr2(expr const & A, expr const & B, expr const & a, expr const & b, expr const & f, expr const & H) { return mk_app({mk_congr2_fn(), A, B, a, b, f, H}); }
-
-expr mk_congr_fn();
-/** \brief (Theorem) {A : Type u}, {B : A -> Type u}, {f g : (Pi x : A, B x)}, {a b : A}, H1 : f = g, H2 : a = b |- Congr(A, B, f, g, a, b, H1, H2) : f a = g b */
-inline expr Congr(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_congr_fn(), A, B, f, g, a, b, H1, H2}); }
-
-expr mk_forall_elim_fn();
-// \brief (Theorem) {A : Type u}, {P : A -> Bool}, H : (Forall A P), a : A |- ForallElim(A, P, H, a) : P a
-inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); }
-
-expr mk_forall_intro_fn();
-// \brief (Theorem) {A : Type u} {P : A -> bool} (H : Pi (x : A), P x) |- ForallIntro(A, P, H) : forall x : A, P
-inline expr ForallIntro(expr const & A, expr const & P, expr const & H) { return mk_app(mk_forall_intro_fn(), A, P, H); }
-
-expr mk_exists_elim_fn();
-// \brief (Theorem) {A : Type U} {P : A -> Bool} {B : Bool} (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a)) |- ExistsElim(A, P, B, H1, H2) : B
-inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr const & H1, expr const & H2) { return mk_app({mk_exists_elim_fn(), A, P, B, H1, H2}); }
-
-expr mk_exists_intro_fn();
-// \brief (Theorem) {A : Type u}, {P : A -> Bool}, a : A,  H : P a |- ExistsIntro(A, P, a, H) : exists x : A, P
-inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); }
-
-/** \brief Add basic theorems to Environment */
-void import_basic_thms(environment const & env);
-}
diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp
index acbf4b3f7..90b0d58df 100644
--- a/src/library/rewriter/rewriter.cpp
+++ b/src/library/rewriter/rewriter.cpp
@@ -14,7 +14,6 @@
 #include "kernel/printer.h"
 #include "kernel/replace_fn.h"
 #include "kernel/type_checker.h"
-#include "library/basic_thms.h"
 #include "library/rewriter/fo_match.h"
 #include "library/rewriter/rewriter.h"
 #include "util/buffer.h"
diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h
index 4ee7097b1..f945763ce 100644
--- a/src/library/rewriter/rewriter.h
+++ b/src/library/rewriter/rewriter.h
@@ -15,7 +15,7 @@ Author: Soonho Kong
 #include "kernel/expr.h"
 #include "kernel/replace_fn.h"
 #include "kernel/type_checker.h"
-#include "library/basic_thms.h"
+#include "kernel/builtin.h"
 #include "library/rewriter/rewriter.h"
 #include "util/exception.h"
 #include "util/scoped_map.h"
diff --git a/src/library/tactic/boolean_tactics.cpp b/src/library/tactic/boolean_tactics.cpp
index 6483337d8..0fafb5ec0 100644
--- a/src/library/tactic/boolean_tactics.cpp
+++ b/src/library/tactic/boolean_tactics.cpp
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/abstract.h"
 #include "kernel/occurs.h"
-#include "library/basic_thms.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/proof_state.h"
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 28efa24c5..440fc95c2 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "kernel/update_expr.h"
 #include "kernel/builtin.h"
 #include "library/kernel_bindings.h"
-#include "library/basic_thms.h"
 #include "library/tactic/tactic.h"
 
 namespace lean {
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index e2197f2b5..d6b61f8e1 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -91,7 +91,7 @@ static struct option g_long_options[] = {
     {"lean",       no_argument,       0, 'l'},
     {"olean",      no_argument,       0, 'b'},
     {"lua",        no_argument,       0, 'u'},
-    {"kernel",     no_argument,       0, 'k'},
+    {"nokernel",   no_argument,       0, 'n'},
     {"path",       no_argument,       0, 'p'},
     {"luahook",    required_argument, 0, 'c'},
     {"githash",    no_argument,       0, 'g'},
@@ -107,13 +107,13 @@ int main(int argc, char ** argv) {
     try {
         lean::save_stack_info();
         lean::register_modules();
-        bool kernel_only    = false;
+        bool no_kernel      = false;
         bool export_objects = false;
         bool trust_imported = false;
         std::string output;
         input_kind default_k = input_kind::Lean; // default
         while (true) {
-            int c = getopt_long(argc, argv, "tklupgvhc:012s:012o:", g_long_options, NULL);
+            int c = getopt_long(argc, argv, "tnlupgvhc:012s:012o:", g_long_options, NULL);
             if (c == -1)
                 break; // end of command line
             switch (c) {
@@ -144,8 +144,8 @@ int main(int argc, char ** argv) {
             case 's':
                 lean::set_thread_stack_size(atoi(optarg)*1024);
                 break;
-            case 'k':
-                kernel_only = true;
+            case 'n':
+                no_kernel = true;
                 break;
             case 'o':
                 output = optarg;
@@ -172,7 +172,7 @@ int main(int argc, char ** argv) {
                 environment env;
                 env->set_trusted_imported(trust_imported);
                 io_state ios;
-                init_frontend(env, ios, kernel_only);
+                init_frontend(env, ios, no_kernel);
                 script_state S;
                 shell sh(env, &S);
                 int status = sh() ? 0 : 1;
@@ -188,7 +188,7 @@ int main(int argc, char ** argv) {
             environment env;
             env->set_trusted_imported(trust_imported);
             io_state    ios;
-            init_frontend(env, ios, kernel_only);
+            init_frontend(env, ios, no_kernel);
             script_state S;
             bool ok = true;
             for (int i = optind; i < argc; i++) {
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 2190b859a..532715d59 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -21,7 +21,6 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/type_checker_justification.h"
 #include "kernel/io_state.h"
-#include "library/basic_thms.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"
 using namespace lean;
diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp
index 5d0be7a6c..19437cda5 100644
--- a/src/tests/library/elaborator/elaborator.cpp
+++ b/src/tests/library/elaborator/elaborator.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/normalizer.h"
 #include "kernel/instantiate.h"
-#include "library/basic_thms.h"
+#include "kernel/builtin.h"
 #include "library/placeholder.h"
 #include "library/arith/arith.h"
 #include "library/elaborator/elaborator.h"
diff --git a/src/tests/library/rewriter/fo_match.cpp b/src/tests/library/rewriter/fo_match.cpp
index 6089fd121..bf59eba75 100644
--- a/src/tests/library/rewriter/fo_match.cpp
+++ b/src/tests/library/rewriter/fo_match.cpp
@@ -10,12 +10,12 @@ Author: Soonho Kong
 #include "kernel/expr.h"
 #include "kernel/metavar.h"
 #include "kernel/printer.h"
+#include "kernel/builtin.h"
 #include "library/all/all.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"
 #include "library/rewriter/fo_match.h"
 #include "library/rewriter/rewriter.h"
-#include "library/basic_thms.h"
 using namespace lean;
 
 using std::cout;
diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp
index 960efef43..17812bc41 100644
--- a/src/tests/library/rewriter/rewriter.cpp
+++ b/src/tests/library/rewriter/rewriter.cpp
@@ -11,12 +11,12 @@ Author: Soonho Kong
 #include "kernel/expr.h"
 #include "kernel/printer.h"
 #include "kernel/io_state.h"
+#include "kernel/builtin.h"
 #include "library/all/all.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"
 #include "library/rewriter/fo_match.h"
 #include "library/rewriter/rewriter.h"
-#include "library/basic_thms.h"
 #include "frontends/lean/frontend.h"
 using namespace lean;
 
diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out
index d11dd8818..8cc99545f 100644
--- a/tests/lean/elab4.lean.expected.out
+++ b/tests/lean/elab4.lean.expected.out
@@ -5,7 +5,7 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Import "basic"
+Import "kernel"
 Import "nat"
 Import "int"
 Import "real"
diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out
index d11dd8818..8cc99545f 100644
--- a/tests/lean/elab5.lean.expected.out
+++ b/tests/lean/elab5.lean.expected.out
@@ -5,7 +5,7 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Import "basic"
+Import "kernel"
 Import "nat"
 Import "int"
 Import "real"