diff --git a/src/kernel/kernel.cpp b/src/kernel/kernel.cpp
deleted file mode 100644
index fcfbddd9ad..0000000000
--- a/src/kernel/kernel.cpp
+++ /dev/null
@@ -1,46 +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/kernel.h"
-#include "kernel/environment.h"
-#include "kernel/abstract.h"
-#include "kernel/io_state.h"
-#include "kernel/decl_macros.h"
-#include "kernel/kernel_decls.cpp"
-
-namespace lean {
-// =======================================
-// Bultin universe variables m and u
-static level u_lvl(name("U"));
-expr const TypeU = Type(u_lvl);
-expr const TypeU1 = Type(u_lvl+1);
-// =======================================
-
-// =======================================
-// Boolean Type
-expr const Bool  = mk_Bool();
-expr const True  = mk_true();
-expr const False = mk_false();
-expr mk_bool_type() { return mk_Bool(); }
-bool is_bool(expr const & t) { return is_Bool(t); }
-// =======================================
-
-expr mk_bool_value(bool v) {
-    return v ? True : False;
-}
-bool is_bool_value(expr const & e) {
-    return is_true(e) || is_false(e);
-}
-bool to_bool(expr const & e) {
-    lean_assert(is_bool_value(e));
-    return e == True;
-}
-// =======================================
-
-void import_kernel(environment const & env, io_state const & ios) {
-    env->import("kernel", ios);
-}
-}
diff --git a/src/kernel/kernel.h b/src/kernel/kernel.h
deleted file mode 100644
index b142288ce2..0000000000
--- a/src/kernel/kernel.h
+++ /dev/null
@@ -1,41 +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/io_state.h"
-#include "kernel/kernel_decls.h"
-
-namespace lean {
-// See src/builtin/kernel.lean for signatures.
-extern expr const TypeU;
-extern expr const TypeU1; // Type (U+1)
-
-/** \brief Return the Lean Boolean type. */
-expr mk_bool_type();
-extern expr const Bool;
-bool is_bool(expr const & e);
-
-/** \brief Create a Lean Boolean value (true/false) */
-expr mk_bool_value(bool v);
-extern expr const True;
-extern expr const False;
-/** \brief Return true iff \c e is a Lean Boolean value. */
-bool is_bool_value(expr const & e);
-/**
-    \brief Convert a Lean Boolean value into a C++ Boolean value.
-    \pre is_bool_value(e)
-*/
-bool to_bool(expr const & e);
-
-inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
-inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
-inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); }
-inline expr Not(expr const & e) { return mk_not(e); }
-inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
-// inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_eq(A, l, r); }
-
-void import_kernel(environment const & env, io_state const & ios);
-}