diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b0a01b442..fafe9d38f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -82,8 +82,9 @@ include_directories(${LEAN_SOURCE_DIR}/util/numerics)
 include_directories(${LEAN_SOURCE_DIR}/util/sexpr)
 include_directories(${LEAN_SOURCE_DIR}/interval)
 include_directories(${LEAN_SOURCE_DIR}/kernel)
-include_directories(${LEAN_SOURCE_DIR}/kernel/arith)
 include_directories(${LEAN_SOURCE_DIR}/library)
+include_directories(${LEAN_SOURCE_DIR}/library/arith)
+include_directories(${LEAN_SOURCE_DIR}/library/import_all)
 include_directories(${LEAN_SOURCE_DIR}/parsers)
 include_directories(${LEAN_SOURCE_DIR}/frontends/lean)
 
@@ -97,10 +98,12 @@ add_subdirectory(interval)
 set(LEAN_LIBS ${LEAN_LIBS} interval)
 add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
-add_subdirectory(kernel/arith)
-set(LEAN_LIBS ${LEAN_LIBS} kernel_arith)
 add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
+add_subdirectory(library/arith)
+set(LEAN_LIBS ${LEAN_LIBS} arithlib)
+add_subdirectory(library/import_all)
+set(LEAN_LIBS ${LEAN_LIBS} import_all)
 add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp
index 22e44bc5c..2cdfc8476 100644
--- a/src/frontends/lean/lean_frontend.cpp
+++ b/src/frontends/lean/lean_frontend.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <atomic>
 #include <unordered_set>
 #include "environment.h"
-#include "toplevel.h"
+#include "import_all.h"
 #include "map.h"
 #include "state.h"
 #include "sstream.h"
@@ -362,7 +362,7 @@ struct frontend::imp {
 };
 
 frontend::frontend():m_imp(new imp(*this)) {
-    init_toplevel(m_imp->m_env);
+    import_all(m_imp->m_env);
     init_builtin_notation(*this);
     m_imp->m_state.set_formatter(mk_pp_formatter(*this));
 }
diff --git a/src/frontends/lean/lean_notation.cpp b/src/frontends/lean/lean_notation.cpp
index f5fdc1a8f..c7e357447 100644
--- a/src/frontends/lean/lean_notation.cpp
+++ b/src/frontends/lean/lean_notation.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "builtin.h"
 #include "basic_thms.h"
 #include "lean_frontend.h"
-#include "arith.h"
+#include "arithlibs.h"
 
 namespace lean {
 /**
diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index 74d02d75a..09d6084da 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "type_checker.h"
 #include "free_vars.h"
 #include "builtin.h"
-#include "arith.h"
+#include "arithlibs.h"
 #include "printer.h"
 #include "state.h"
 #include "option_declarations.h"
diff --git a/src/kernel/arith/CMakeLists.txt b/src/kernel/arith/CMakeLists.txt
deleted file mode 100644
index 0f58d78cf..000000000
--- a/src/kernel/arith/CMakeLists.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-add_library(kernel_arith arith.cpp)
-target_link_libraries(kernel_arith ${LEAN_LIBS})
diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
deleted file mode 100644
index b6700cedc..000000000
--- a/src/kernel/arith/arith.cpp
+++ /dev/null
@@ -1,437 +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 "builtin.h"
-#include "arith.h"
-#include "abstract.h"
-#include "value.h"
-#include "environment.h"
-
-namespace lean {
-class num_type_value : public type_value {
-    name m_unicode;
-public:
-    num_type_value(name const & n, name const & u):type_value(n), m_unicode(u) {}
-    virtual ~num_type_value() {}
-    virtual name get_unicode_name() const { return m_unicode; }
-};
-
-// =======================================
-// Natural numbers
-class nat_type_value : public num_type_value {
-public:
-    nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
-};
-expr const Nat = mk_value(*(new nat_type_value()));
-expr mk_nat_type() { return Nat; }
-
-class nat_value_value : public value {
-    mpz m_val;
-public:
-    nat_value_value(mpz const & v):m_val(v) { lean_assert(v >= 0); }
-    virtual ~nat_value_value() {}
-    virtual expr get_type() const { return Nat; }
-    virtual name get_name() const { return name{"Nat", "numeral"}; }
-    virtual bool operator==(value const & other) const {
-        nat_value_value const * _other = dynamic_cast<nat_value_value const*>(&other);
-        return _other && _other->m_val == m_val;
-    }
-    virtual void display(std::ostream & out) const { out << m_val; }
-    virtual format pp() const { return format(m_val); }
-    virtual format pp(bool unicode) const { return pp(); }
-    virtual unsigned hash() const { return m_val.hash(); }
-    mpz const & get_num() const { return m_val; }
-};
-
-expr mk_nat_value(mpz const & v) {
-    return mk_value(*(new nat_value_value(v)));
-}
-
-bool is_nat_value(expr const & e) {
-    return is_value(e) && dynamic_cast<nat_value_value const *>(&to_value(e)) != nullptr;
-}
-
-mpz const & nat_value_numeral(expr const & e) {
-    lean_assert(is_nat_value(e));
-    return static_cast<nat_value_value const &>(to_value(e)).get_num();
-}
-
-template<char const * Name, typename F>
-class nat_bin_op : public const_value {
-public:
-    nat_bin_op():const_value(name("Nat", Name), Nat >> (Nat >> Nat)) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
-            r = mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2])));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-
-constexpr char nat_add_name[] = "add";
-struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
-typedef nat_bin_op<nat_add_name, nat_add_eval> nat_add_value;
-MK_BUILTIN(nat_add_fn, nat_add_value);
-
-constexpr char nat_mul_name[] = "mul";
-struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
-typedef nat_bin_op<nat_mul_name, nat_mul_eval> nat_mul_value;
-MK_BUILTIN(nat_mul_fn, nat_mul_value);
-
-class nat_le_value : public const_value {
-public:
-    nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
-            r = mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2]));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-MK_BUILTIN(nat_le_fn, nat_le_value);
-
-MK_CONSTANT(nat_ge_fn, name({"Nat", "ge"}));
-MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"}));
-MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"}));
-MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
-MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
-MK_CONSTANT(nat_id_fn, name({"Nat", "id"}));
-// =======================================
-
-// =======================================
-// Integers
-class int_type_value : public num_type_value {
-public:
-    int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
-};
-expr const Int = mk_value(*(new int_type_value()));
-expr mk_int_type() { return Int; }
-
-class int_value_value : public value {
-    mpz m_val;
-public:
-    int_value_value(mpz const & v):m_val(v) {}
-    virtual ~int_value_value() {}
-    virtual expr get_type() const { return Int; }
-    virtual name get_name() const { return name{"Int", "numeral"}; }
-    virtual bool operator==(value const & other) const {
-        int_value_value const * _other = dynamic_cast<int_value_value const*>(&other);
-        return _other && _other->m_val == m_val;
-    }
-    virtual void display(std::ostream & out) const { out << m_val; }
-    virtual format pp() const { return format(m_val); }
-    virtual format pp(bool unicode) const { return pp(); }
-    virtual unsigned hash() const { return m_val.hash(); }
-    mpz const & get_num() const { return m_val; }
-};
-
-expr mk_int_value(mpz const & v) {
-    return mk_value(*(new int_value_value(v)));
-}
-
-bool is_int_value(expr const & e) {
-    return is_value(e) && dynamic_cast<int_value_value const *>(&to_value(e)) != nullptr;
-}
-
-mpz const & int_value_numeral(expr const & e) {
-    lean_assert(is_int_value(e));
-    return static_cast<int_value_value const &>(to_value(e)).get_num();
-}
-
-template<char const * Name, typename F>
-class int_bin_op : public const_value {
-public:
-    int_bin_op():const_value(name("Int", Name), Int >> (Int >> Int)) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
-            r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-
-constexpr char int_add_name[] = "add";
-struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
-typedef int_bin_op<int_add_name, int_add_eval> int_add_value;
-MK_BUILTIN(int_add_fn, int_add_value);
-
-constexpr char int_mul_name[] = "mul";
-struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
-typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
-MK_BUILTIN(int_mul_fn, int_mul_value);
-
-constexpr char int_div_name[] = "div";
-struct int_div_eval {
-    mpz operator()(mpz const & v1, mpz const & v2) {
-        if (v2.is_zero())
-            return v2;
-        else
-            return v1 / v2;
-    };
-};
-typedef int_bin_op<int_div_name, int_div_eval> int_div_value;
-MK_BUILTIN(int_div_fn, int_div_value);
-
-class int_le_value : public const_value {
-public:
-    int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
-            r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-MK_BUILTIN(int_le_fn, int_le_value);
-
-MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
-MK_CONSTANT(int_neg_fn, name({"Int", "neg"}));
-MK_CONSTANT(int_mod_fn, name({"Int", "mod"}));
-MK_CONSTANT(int_divides_fn, name({"Int", "divides"}));
-MK_CONSTANT(int_abs_fn, name({"Int", "abs"}));
-MK_CONSTANT(int_ge_fn, name({"Int", "ge"}));
-MK_CONSTANT(int_lt_fn, name({"Int", "lt"}));
-MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
-// =======================================
-
-// =======================================
-// Reals
-class real_type_value : public num_type_value {
-public:
-    real_type_value():num_type_value("Real", "\u211D") /* ℝ */ {}
-};
-expr const Real = mk_value(*(new real_type_value()));
-expr mk_real_type() { return Real; }
-
-class real_value_value : public value {
-    mpq m_val;
-public:
-    real_value_value(mpq const & v):m_val(v) {}
-    virtual ~real_value_value() {}
-    virtual expr get_type() const { return Real; }
-    virtual name get_name() const { return name{"Real", "numeral"}; }
-    virtual bool operator==(value const & other) const {
-        real_value_value const * _other = dynamic_cast<real_value_value const*>(&other);
-        return _other && _other->m_val == m_val;
-    }
-    virtual void display(std::ostream & out) const { out << m_val; }
-    virtual format pp() const { return format(m_val); }
-    virtual format pp(bool unicode) const { return pp(); }
-    virtual unsigned hash() const { return m_val.hash(); }
-    mpq const & get_num() const { return m_val; }
-};
-
-expr mk_real_value(mpq const & v) {
-    return mk_value(*(new real_value_value(v)));
-}
-
-bool is_real_value(expr const & e) {
-    return is_value(e) && dynamic_cast<real_value_value const *>(&to_value(e)) != nullptr;
-}
-
-mpq const & real_value_numeral(expr const & e) {
-    lean_assert(is_real_value(e));
-    return static_cast<real_value_value const &>(to_value(e)).get_num();
-}
-
-template<char const * Name, typename F>
-class real_bin_op : public const_value {
-public:
-    real_bin_op():const_value(name("Real", Name), Real >> (Real >> Real)) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
-            r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2])));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-
-constexpr char real_add_name[] = "add";
-struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; };
-typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
-MK_BUILTIN(real_add_fn, real_add_value);
-
-constexpr char real_mul_name[] = "mul";
-struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; };
-typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
-MK_BUILTIN(real_mul_fn, real_mul_value);
-
-constexpr char real_div_name[] = "div";
-struct real_div_eval {
-    mpq operator()(mpq const & v1, mpq const & v2) {
-        if (v2.is_zero())
-            return v2;
-        else
-            return v1 / v2;
-    };
-};
-typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
-MK_BUILTIN(real_div_fn, real_div_value);
-
-class real_le_value : public const_value {
-public:
-    real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
-            r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2]));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-MK_BUILTIN(real_le_fn, real_le_value);
-
-MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
-MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
-MK_CONSTANT(real_abs_fn, name({"Real", "abs"}));
-MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
-MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
-MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
-
-MK_CONSTANT(exp_fn, name("exp"));
-MK_CONSTANT(log_fn, name("log"));
-
-MK_CONSTANT(real_pi, name("\u03C0")); // lower case pi
-MK_CONSTANT(sin_fn, name("sin"));
-MK_CONSTANT(cos_fn, name("cos"));
-MK_CONSTANT(tan_fn, name("tan"));
-MK_CONSTANT(cot_fn, name("cot"));
-MK_CONSTANT(sec_fn, name("sec"));
-MK_CONSTANT(csc_fn, name("csc"));
-
-MK_CONSTANT(sinh_fn, name("sinh"));
-MK_CONSTANT(cosh_fn, name("cosh"));
-MK_CONSTANT(tanh_fn, name("tanh"));
-MK_CONSTANT(coth_fn, name("coth"));
-MK_CONSTANT(sech_fn, name("sech"));
-MK_CONSTANT(csch_fn, name("csch"));
-// =======================================
-
-// =======================================
-// Coercions
-class nat_to_int_value : public const_value {
-public:
-    nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 2 && is_nat_value(args[1])) {
-            r = mk_int_value(nat_value_numeral(args[1]));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
-
-class int_to_real_value : public const_value {
-public:
-    int_to_real_value():const_value("int_to_real", Int >> Real) {}
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
-        if (num_args == 2 && is_int_value(args[1])) {
-            r = mk_real_value(mpq(int_value_numeral(args[1])));
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-MK_BUILTIN(int_to_real_fn,  int_to_real_value);
-MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
-// =======================================
-
-void add_arith_theory(environment & env) {
-    expr nn_b = Nat >> (Nat >> Bool);
-    expr ii_b = Int >> (Int >> Bool);
-    expr ii_i = Int >> (Int >> Int);
-    expr rr_b = Real >> (Real >> Bool);
-    expr rr_r = Real >> (Real >> Real);
-    expr i_i  = Int >> Int;
-    expr r_r  = Real >> Real;
-    expr x    = Const("x");
-    expr y    = Const("y");
-
-    env.add_builtin(Nat);
-    env.add_builtin_set(nVal(0));
-    env.add_builtin(mk_nat_add_fn());
-    env.add_builtin(mk_nat_mul_fn());
-    env.add_builtin(mk_nat_le_fn());
-
-    env.add_builtin(Int);
-    env.add_builtin_set(iVal(0));
-    env.add_builtin(mk_int_add_fn());
-    env.add_builtin(mk_int_mul_fn());
-    env.add_builtin(mk_int_div_fn());
-    env.add_builtin(mk_int_le_fn());
-
-    env.add_builtin(Real);
-    env.add_builtin_set(rVal(0));
-    env.add_builtin(mk_real_add_fn());
-    env.add_builtin(mk_real_mul_fn());
-    env.add_builtin(mk_real_div_fn());
-    env.add_builtin(mk_real_le_fn());
-
-    env.add_builtin(mk_nat_to_int_fn());
-    env.add_builtin(mk_int_to_real_fn());
-
-    env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
-    env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
-    env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
-    env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
-
-    env.add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
-    env.add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
-    env.add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
-    env.add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
-    env.add_definition(int_ge_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, iLe(y, x)));
-    env.add_definition(int_lt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
-    env.add_definition(int_gt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
-    env.add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
-
-    env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
-    env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
-
-    env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y))));
-    env.add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x)));
-    env.add_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x))));
-    env.add_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));
-    env.add_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
-    env.add_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
-
-    env.add_var(exp_fn_name, r_r);
-    env.add_var(log_fn_name, r_r);
-
-    env.add_var(real_pi_name, Real);
-    env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
-    env.add_var(sin_fn_name, r_r);
-    env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
-    env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x))));
-    env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x))));
-    env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cos(x))));
-    env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sin(x))));
-
-    env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
-                                                              rMul(rVal(2), Exp(rNeg(x))))));
-    env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
-                                                              rMul(rVal(2), Exp(rNeg(x))))));
-    env.add_definition(tanh_fn_name, r_r, Fun({x,Real}, rDiv(Sinh(x), Cosh(x))));
-    env.add_definition(coth_fn_name, r_r, Fun({x,Real}, rDiv(Cosh(x), Sinh(x))));
-    env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cosh(x))));
-    env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sinh(x))));
-
-    env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
-}
-}
diff --git a/src/kernel/arith/arith.h b/src/kernel/arith/arith.h
deleted file mode 100644
index efd5938df..000000000
--- a/src/kernel/arith/arith.h
+++ /dev/null
@@ -1,216 +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 "expr.h"
-#include "builtin.h"
-#include "mpz.h"
-#include "mpq.h"
-
-namespace lean {
-// =======================================
-// Natural numbers
-expr mk_nat_type();
-extern expr const Nat;
-
-expr mk_nat_value(mpz const & v);
-inline expr mk_nat_value(unsigned v) { return mk_nat_value(mpz(v)); }
-inline expr nVal(unsigned v) { return mk_nat_value(v); }
-bool is_nat_value(expr const & e);
-mpz const & nat_value_numeral(expr const & e);
-
-/** \brief Nat::add : Nat -> Nat -> Nat */
-expr mk_nat_add_fn();
-inline expr nAdd(expr const & e1, expr const & e2) { return mk_app(mk_nat_add_fn(), e1, e2); }
-
-/** \brief Nat::sub : Nat -> Nat -> Int */
-expr mk_nat_sub_fn();
-inline expr nSub(expr const & e1, expr const & e2) { return mk_app(mk_nat_sub_fn(), e1, e2); }
-
-/** \brief Nat::neg : Nat -> Int */
-expr mk_nat_neg_fn();
-inline expr nNeg(expr const & e1, expr const & e2) { return mk_app(mk_nat_neg_fn(), e1, e2); }
-
-/** \brief Nat::mul : Nat -> Nat -> Nat */
-expr mk_nat_mul_fn();
-inline expr nMul(expr const & e1, expr const & e2) { return mk_app(mk_nat_mul_fn(), e1, e2); }
-
-/** \brief Nat::le : Nat -> Nat -> Bool */
-expr mk_nat_le_fn();
-inline expr nLe(expr const & e1, expr const & e2) { return mk_app(mk_nat_le_fn(), e1, e2); }
-
-/** \brief Nat::ge : Nat -> Nat -> Bool */
-expr mk_nat_ge_fn();
-inline expr nGe(expr const & e1, expr const & e2) { return mk_app(mk_nat_ge_fn(), e1, e2); }
-
-/** \brief Nat::lt : Nat -> Nat -> Bool */
-expr mk_nat_lt_fn();
-inline expr nLt(expr const & e1, expr const & e2) { return mk_app(mk_nat_lt_fn(), e1, e2); }
-
-/** \brief Nat::gt : Nat -> Nat -> Bool */
-expr mk_nat_gt_fn();
-inline expr nGt(expr const & e1, expr const & e2) { return mk_app(mk_nat_gt_fn(), e1, e2); }
-
-expr mk_nat_id_fn();
-inline expr nId(expr const & e) { return mk_app(mk_nat_id_fn(), e); }
-
-inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(Nat, c, t, e); }
-// =======================================
-
-// =======================================
-// Integers
-expr mk_int_type();
-extern expr const Int;
-
-expr mk_int_value(mpz const & v);
-inline expr mk_int_value(int v) { return mk_int_value(mpz(v)); }
-inline expr iVal(int v) { return mk_int_value(v); }
-bool is_int_value(expr const & e);
-mpz const & int_value_numeral(expr const & e);
-
-expr mk_int_add_fn();
-inline expr iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn(), e1, e2); }
-
-expr mk_int_sub_fn();
-inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); }
-
-expr mk_int_neg_fn();
-inline expr iNeg(expr const & e) { return mk_app(mk_int_neg_fn(), e); }
-
-expr mk_int_mul_fn();
-inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); }
-
-expr mk_int_div_fn();
-inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); }
-
-expr mk_int_mod_fn();
-inline expr iMod(expr const & e1, expr const & e2) { return mk_app(mk_int_mod_fn(), e1, e2); }
-
-expr mk_int_divides_fn();
-inline expr iDivides(expr const & e1, expr const & e2) { return mk_app(mk_int_divides_fn(), e1, e2); }
-
-expr mk_int_abs_fn();
-inline expr iAbs(expr const & e) { return mk_app(mk_int_abs_fn(), e); }
-
-expr mk_int_le_fn();
-inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); }
-
-expr mk_int_ge_fn();
-inline expr iGe(expr const & e1, expr const & e2) { return mk_app(mk_int_ge_fn(), e1, e2); }
-
-expr mk_int_lt_fn();
-inline expr iLt(expr const & e1, expr const & e2) { return mk_app(mk_int_lt_fn(), e1, e2); }
-
-expr mk_int_gt_fn();
-inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); }
-
-inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); }
-// =======================================
-
-// =======================================
-// Reals
-expr mk_real_type();
-extern expr const Real;
-
-expr mk_real_value(mpq const & v);
-inline expr mk_real_value(int v) { return mk_real_value(mpq(v)); }
-inline expr rVal(int v) { return mk_real_value(v); }
-bool is_real_value(expr const & e);
-mpq const & real_value_numeral(expr const & e);
-
-expr mk_real_add_fn();
-inline expr rAdd(expr const & e1, expr const & e2) { return mk_app(mk_real_add_fn(), e1, e2); }
-
-expr mk_real_sub_fn();
-inline expr rSub(expr const & e1, expr const & e2) { return mk_app(mk_real_sub_fn(), e1, e2); }
-
-expr mk_real_neg_fn();
-inline expr rNeg(expr const & e) { return mk_app(mk_real_neg_fn(), e); }
-
-expr mk_real_mul_fn();
-inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_fn(), e1, e2); }
-
-expr mk_real_div_fn();
-inline expr rDiv(expr const & e1, expr const & e2) { return mk_app(mk_real_div_fn(), e1, e2); }
-
-expr mk_real_abs_fn();
-inline expr rAbs(expr const & e) { return mk_app(mk_real_abs_fn(), e); }
-
-expr mk_real_le_fn();
-inline expr rLe(expr const & e1, expr const & e2) { return mk_app(mk_real_le_fn(), e1, e2); }
-
-expr mk_real_ge_fn();
-inline expr rGe(expr const & e1, expr const & e2) { return mk_app(mk_real_ge_fn(), e1, e2); }
-
-expr mk_real_lt_fn();
-inline expr rLt(expr const & e1, expr const & e2) { return mk_app(mk_real_lt_fn(), e1, e2); }
-
-expr mk_real_gt_fn();
-inline expr rGt(expr const & e1, expr const & e2) { return mk_app(mk_real_gt_fn(), e1, e2); }
-
-inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(Real, c, t, e); }
-
-expr mk_exp_fn();
-inline expr Exp(expr const & e) { return mk_app(mk_exp_fn(), e); }
-
-expr mk_log_fn();
-inline expr Log(expr const & e) { return mk_app(mk_log_fn(), e); }
-// =======================================
-
-// =======================================
-// Transcendental and Hyperbolic
-expr mk_real_pi();
-
-expr mk_sin_fn();
-inline expr Sin(expr const & e) { return mk_app(mk_sin_fn(), e); }
-
-expr mk_cos_fn();
-inline expr Cos(expr const & e) { return mk_app(mk_cos_fn(), e); }
-
-expr mk_tan_fn();
-inline expr Tan(expr const & e) { return mk_app(mk_tan_fn(), e); }
-
-expr mk_cot_fn();
-inline expr Cot(expr const & e) { return mk_app(mk_cot_fn(), e); }
-
-expr mk_sec_fn();
-inline expr Sec(expr const & e) { return mk_app(mk_sec_fn(), e); }
-
-expr mk_csc_fn();
-inline expr Csc(expr const & e) { return mk_app(mk_csc_fn(), e); }
-
-expr mk_sinh_fn();
-inline expr Sinh(expr const & e) { return mk_app(mk_sinh_fn(), e); }
-
-expr mk_cosh_fn();
-inline expr Cosh(expr const & e) { return mk_app(mk_cosh_fn(), e); }
-
-expr mk_tanh_fn();
-inline expr Tanh(expr const & e) { return mk_app(mk_tanh_fn(), e); }
-
-expr mk_coth_fn();
-inline expr Coth(expr const & e) { return mk_app(mk_coth_fn(), e); }
-
-expr mk_sech_fn();
-inline expr Sech(expr const & e) { return mk_app(mk_sech_fn(), e); }
-
-expr mk_csch_fn();
-inline expr Csch(expr const & e) { return mk_app(mk_csch_fn(), e); }
-// =======================================
-
-// =======================================
-// Coercions
-expr mk_nat_to_int_fn();
-inline expr n2i(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
-expr mk_int_to_real_fn();
-inline expr i2r(expr const & e) { return mk_app(mk_int_to_real_fn(), e); }
-expr mk_nat_to_real_fn();
-inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); }
-// =======================================
-
-class environment;
-void add_arith_theory(environment & env);
-}
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index b63182861..5d8039fbf 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
-  toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
+  printer.cpp formatter.cpp context_to_lambda.cpp
   state.cpp metavar.cpp update_expr.cpp kernel_exception_formatter.cpp)
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/arith/CMakeLists.txt b/src/library/arith/CMakeLists.txt
new file mode 100644
index 000000000..8a67eab8c
--- /dev/null
+++ b/src/library/arith/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_library(arithlib natlib.cpp intlib.cpp reallib.cpp specialfnlib.cpp arithlibs.cpp)
+target_link_libraries(arithlib ${LEAN_LIBS})
diff --git a/src/library/arith/arithlibs.cpp b/src/library/arith/arithlibs.cpp
new file mode 100644
index 000000000..ad54417f7
--- /dev/null
+++ b/src/library/arith/arithlibs.cpp
@@ -0,0 +1,17 @@
+/*
+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 "arithlibs.h"
+
+namespace lean {
+void import_arithlibs(environment & env) {
+    import_natlib(env);
+    import_intlib(env);
+    import_reallib(env);
+    import_int_to_real_coercions(env);
+    import_specialfnlib(env);
+}
+}
diff --git a/src/library/arith/arithlibs.h b/src/library/arith/arithlibs.h
new file mode 100644
index 000000000..2584183f9
--- /dev/null
+++ b/src/library/arith/arithlibs.h
@@ -0,0 +1,19 @@
+/*
+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 "natlib.h"
+#include "intlib.h"
+#include "reallib.h"
+#include "specialfnlib.h"
+
+namespace lean {
+class environment;
+/**
+   \brief Import all arithmetic related builtin libraries.
+*/
+void import_arithlibs(environment & env);
+}
diff --git a/src/library/arith/intlib.cpp b/src/library/arith/intlib.cpp
new file mode 100644
index 000000000..31ae459e3
--- /dev/null
+++ b/src/library/arith/intlib.cpp
@@ -0,0 +1,158 @@
+/*
+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 "intlib.h"
+#include "natlib.h"
+#include "numtype.h"
+#include "abstract.h"
+#include "environment.h"
+
+namespace lean {
+class int_type_value : public num_type_value {
+public:
+    int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
+};
+expr const Int = mk_value(*(new int_type_value()));
+expr mk_int_type() { return Int; }
+
+class int_value_value : public value {
+    mpz m_val;
+public:
+    int_value_value(mpz const & v):m_val(v) {}
+    virtual ~int_value_value() {}
+    virtual expr get_type() const { return Int; }
+    virtual name get_name() const { return name{"Int", "numeral"}; }
+    virtual bool operator==(value const & other) const {
+        int_value_value const * _other = dynamic_cast<int_value_value const*>(&other);
+        return _other && _other->m_val == m_val;
+    }
+    virtual void display(std::ostream & out) const { out << m_val; }
+    virtual format pp() const { return format(m_val); }
+    virtual format pp(bool unicode) const { return pp(); }
+    virtual unsigned hash() const { return m_val.hash(); }
+    mpz const & get_num() const { return m_val; }
+};
+
+expr mk_int_value(mpz const & v) {
+    return mk_value(*(new int_value_value(v)));
+}
+
+bool is_int_value(expr const & e) {
+    return is_value(e) && dynamic_cast<int_value_value const *>(&to_value(e)) != nullptr;
+}
+
+mpz const & int_value_numeral(expr const & e) {
+    lean_assert(is_int_value(e));
+    return static_cast<int_value_value const &>(to_value(e)).get_num();
+}
+
+template<char const * Name, typename F>
+class int_bin_op : public const_value {
+public:
+    int_bin_op():const_value(name("Int", Name), Int >> (Int >> Int)) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
+            r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+
+constexpr char int_add_name[] = "add";
+struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
+typedef int_bin_op<int_add_name, int_add_eval> int_add_value;
+MK_BUILTIN(int_add_fn, int_add_value);
+
+constexpr char int_mul_name[] = "mul";
+struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
+typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
+MK_BUILTIN(int_mul_fn, int_mul_value);
+
+constexpr char int_div_name[] = "div";
+struct int_div_eval {
+    mpz operator()(mpz const & v1, mpz const & v2) {
+        if (v2.is_zero())
+            return v2;
+        else
+            return v1 / v2;
+    };
+};
+typedef int_bin_op<int_div_name, int_div_eval> int_div_value;
+MK_BUILTIN(int_div_fn, int_div_value);
+
+class int_le_value : public const_value {
+public:
+    int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
+            r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+MK_BUILTIN(int_le_fn, int_le_value);
+
+MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
+MK_CONSTANT(int_neg_fn, name({"Int", "neg"}));
+MK_CONSTANT(int_mod_fn, name({"Int", "mod"}));
+MK_CONSTANT(int_divides_fn, name({"Int", "divides"}));
+MK_CONSTANT(int_abs_fn, name({"Int", "abs"}));
+MK_CONSTANT(int_ge_fn, name({"Int", "ge"}));
+MK_CONSTANT(int_lt_fn, name({"Int", "lt"}));
+MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
+
+class nat_to_int_value : public const_value {
+public:
+    nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 2 && is_nat_value(args[1])) {
+            r = mk_int_value(nat_value_numeral(args[1]));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
+
+MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
+MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
+
+void import_intlib(environment & env) {
+    if (env.find_object(to_value(Int).get_name()))
+        return;
+    import_natlib(env);
+    expr i_i  = Int >> Int;
+    expr ii_b = Int >> (Int >> Bool);
+    expr ii_i = Int >> (Int >> Int);
+    expr x    = Const("x");
+    expr y    = Const("y");
+
+    env.add_builtin(Int);
+    env.add_builtin_set(iVal(0));
+    env.add_builtin(mk_int_add_fn());
+    env.add_builtin(mk_int_mul_fn());
+    env.add_builtin(mk_int_div_fn());
+    env.add_builtin(mk_int_le_fn());
+    env.add_builtin(mk_nat_to_int_fn());
+
+    env.add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
+    env.add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
+    env.add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
+    env.add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
+    env.add_definition(int_ge_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, iLe(y, x)));
+    env.add_definition(int_lt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
+    env.add_definition(int_gt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
+    env.add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
+
+    env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
+    env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
+}
+}
diff --git a/src/library/arith/intlib.h b/src/library/arith/intlib.h
new file mode 100644
index 000000000..452b6c46d
--- /dev/null
+++ b/src/library/arith/intlib.h
@@ -0,0 +1,93 @@
+/*
+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 "expr.h"
+#include "builtin.h"
+#include "mpz.h"
+
+namespace lean {
+/** \brief Integer numbers type */
+expr mk_int_type();
+extern expr const Int;
+
+/** \brief Return the value of type Integer that represents \c v. */
+expr mk_int_value(mpz const & v);
+inline expr mk_int_value(int v) { return mk_int_value(mpz(v)); }
+inline expr iVal(int v) { return mk_int_value(v); }
+bool is_int_value(expr const & e);
+mpz const & int_value_numeral(expr const & e);
+
+/** \brief Addition, Int::add : Int -> Int -> Int */
+expr mk_int_add_fn();
+inline expr iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn(), e1, e2); }
+
+/** \brief Subtraction, Int::sub : Int -> Int -> Int */
+expr mk_int_sub_fn();
+inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); }
+
+/** \brief Unary minus, Int::neg : Int -> Int */
+expr mk_int_neg_fn();
+inline expr iNeg(expr const & e) { return mk_app(mk_int_neg_fn(), e); }
+
+/** \brief Multiplication, Int::mul : Int -> Int -> Int */
+expr mk_int_mul_fn();
+inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); }
+
+/** \brief Integer division, Int::mul : Int -> Int -> Int */
+expr mk_int_div_fn();
+inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); }
+
+/** \brief Modulus, Int::mul : Int -> Int -> Int */
+expr mk_int_mod_fn();
+inline expr iMod(expr const & e1, expr const & e2) { return mk_app(mk_int_mod_fn(), e1, e2); }
+
+/** \brief Divides predicate, Int::mul : Int -> Int -> Bool */
+expr mk_int_divides_fn();
+inline expr iDivides(expr const & e1, expr const & e2) { return mk_app(mk_int_divides_fn(), e1, e2); }
+
+/** \brief Absolute value function, Int::abs : Int -> Int */
+expr mk_int_abs_fn();
+inline expr iAbs(expr const & e) { return mk_app(mk_int_abs_fn(), e); }
+
+/** \brief Less than or equal to, Int::le : Int -> Int -> Bool */
+expr mk_int_le_fn();
+inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); }
+
+/** \brief Greater than or equal to, Int::ge : Int -> Int -> Bool */
+expr mk_int_ge_fn();
+inline expr iGe(expr const & e1, expr const & e2) { return mk_app(mk_int_ge_fn(), e1, e2); }
+
+/** \brief Less than, Int::lt : Int -> Int -> Bool */
+expr mk_int_lt_fn();
+inline expr iLt(expr const & e1, expr const & e2) { return mk_app(mk_int_lt_fn(), e1, e2); }
+
+/** \brief Greater than, Int::gt : Int -> Int -> Bool */
+expr mk_int_gt_fn();
+inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); }
+
+/** \brief If-then-else for integers */
+inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); }
+
+/** \brief Coercion from natural to integer */
+expr mk_nat_to_int_fn();
+inline expr n2i(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
+
+/** \brief Subtraction (for naturals), Nat::sub : Nat -> Nat -> Int */
+expr mk_nat_sub_fn();
+inline expr nSub(expr const & e1, expr const & e2) { return mk_app(mk_nat_sub_fn(), e1, e2); }
+
+/** \brief Unary minus (for naturals), Nat::neg : Nat -> Int */
+expr mk_nat_neg_fn();
+inline expr nNeg(expr const & e1, expr const & e2) { return mk_app(mk_nat_neg_fn(), e1, e2); }
+
+class environment;
+/**
+    \brief Import Integer number library in the given environment (if it has not been imported already).
+    It will also load the natural number library.
+*/
+void import_intlib(environment & env);
+}
diff --git a/src/library/arith/natlib.cpp b/src/library/arith/natlib.cpp
new file mode 100644
index 000000000..6f975337f
--- /dev/null
+++ b/src/library/arith/natlib.cpp
@@ -0,0 +1,112 @@
+/*
+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 "natlib.h"
+#include "numtype.h"
+#include "abstract.h"
+#include "environment.h"
+
+namespace lean {
+class nat_type_value : public num_type_value {
+public:
+    nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
+};
+expr const Nat = mk_value(*(new nat_type_value()));
+expr mk_nat_type() { return Nat; }
+
+class nat_value_value : public value {
+    mpz m_val;
+public:
+    nat_value_value(mpz const & v):m_val(v) { lean_assert(v >= 0); }
+    virtual ~nat_value_value() {}
+    virtual expr get_type() const { return Nat; }
+    virtual name get_name() const { return name{"Nat", "numeral"}; }
+    virtual bool operator==(value const & other) const {
+        nat_value_value const * _other = dynamic_cast<nat_value_value const*>(&other);
+        return _other && _other->m_val == m_val;
+    }
+    virtual void display(std::ostream & out) const { out << m_val; }
+    virtual format pp() const { return format(m_val); }
+    virtual format pp(bool unicode) const { return pp(); }
+    virtual unsigned hash() const { return m_val.hash(); }
+    mpz const & get_num() const { return m_val; }
+};
+
+expr mk_nat_value(mpz const & v) {
+    return mk_value(*(new nat_value_value(v)));
+}
+
+bool is_nat_value(expr const & e) {
+    return is_value(e) && dynamic_cast<nat_value_value const *>(&to_value(e)) != nullptr;
+}
+
+mpz const & nat_value_numeral(expr const & e) {
+    lean_assert(is_nat_value(e));
+    return static_cast<nat_value_value const &>(to_value(e)).get_num();
+}
+
+template<char const * Name, typename F>
+class nat_bin_op : public const_value {
+public:
+    nat_bin_op():const_value(name("Nat", Name), Nat >> (Nat >> Nat)) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
+            r = mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2])));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+
+constexpr char nat_add_name[] = "add";
+struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
+typedef nat_bin_op<nat_add_name, nat_add_eval> nat_add_value;
+MK_BUILTIN(nat_add_fn, nat_add_value);
+
+constexpr char nat_mul_name[] = "mul";
+struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
+typedef nat_bin_op<nat_mul_name, nat_mul_eval> nat_mul_value;
+MK_BUILTIN(nat_mul_fn, nat_mul_value);
+
+class nat_le_value : public const_value {
+public:
+    nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
+            r = mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2]));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+MK_BUILTIN(nat_le_fn, nat_le_value);
+
+MK_CONSTANT(nat_ge_fn,  name({"Nat", "ge"}));
+MK_CONSTANT(nat_lt_fn,  name({"Nat", "lt"}));
+MK_CONSTANT(nat_gt_fn,  name({"Nat", "gt"}));
+MK_CONSTANT(nat_id_fn,  name({"Nat", "id"}));
+
+void import_natlib(environment & env) {
+    if (env.find_object(to_value(Nat).get_name()))
+        return;
+    expr nn_b = Nat >> (Nat >> Bool);
+    expr x    = Const("x");
+    expr y    = Const("y");
+
+    env.add_builtin(Nat);
+    env.add_builtin_set(nVal(0));
+    env.add_builtin(mk_nat_add_fn());
+    env.add_builtin(mk_nat_mul_fn());
+    env.add_builtin(mk_nat_le_fn());
+
+    env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
+    env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
+    env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
+    env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
+}
+}
diff --git a/src/library/arith/natlib.h b/src/library/arith/natlib.h
new file mode 100644
index 000000000..401e08380
--- /dev/null
+++ b/src/library/arith/natlib.h
@@ -0,0 +1,58 @@
+/*
+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 "expr.h"
+#include "builtin.h"
+#include "mpz.h"
+
+namespace lean {
+/** \brief Natural numbers type */
+expr mk_nat_type();
+extern expr const Nat;
+
+/** \brief Return the value of type Natural number that represents \c v. */
+expr mk_nat_value(mpz const & v);
+inline expr mk_nat_value(unsigned v) { return mk_nat_value(mpz(v)); }
+inline expr nVal(unsigned v) { return mk_nat_value(v); }
+bool is_nat_value(expr const & e);
+mpz const & nat_value_numeral(expr const & e);
+
+/** \brief Addition, Nat::add : Nat -> Nat -> Nat */
+expr mk_nat_add_fn();
+inline expr nAdd(expr const & e1, expr const & e2) { return mk_app(mk_nat_add_fn(), e1, e2); }
+
+/** \brief Multiplication, Nat::mul : Nat -> Nat -> Nat */
+expr mk_nat_mul_fn();
+inline expr nMul(expr const & e1, expr const & e2) { return mk_app(mk_nat_mul_fn(), e1, e2); }
+
+/** \brief Less than or equal to, Nat::le : Nat -> Nat -> Bool */
+expr mk_nat_le_fn();
+inline expr nLe(expr const & e1, expr const & e2) { return mk_app(mk_nat_le_fn(), e1, e2); }
+
+/** \brief Greater than or equal to, Nat::ge : Nat -> Nat -> Bool */
+expr mk_nat_ge_fn();
+inline expr nGe(expr const & e1, expr const & e2) { return mk_app(mk_nat_ge_fn(), e1, e2); }
+
+/** \brief Less than, Nat::lt : Nat -> Nat -> Bool */
+expr mk_nat_lt_fn();
+inline expr nLt(expr const & e1, expr const & e2) { return mk_app(mk_nat_lt_fn(), e1, e2); }
+
+/** \brief Greater than, Nat::gt : Nat -> Nat -> Bool */
+expr mk_nat_gt_fn();
+inline expr nGt(expr const & e1, expr const & e2) { return mk_app(mk_nat_gt_fn(), e1, e2); }
+
+/** \brief Identity function for natural numbers, Nat::id : Nat -> Nat */
+expr mk_nat_id_fn();
+inline expr nId(expr const & e) { return mk_app(mk_nat_id_fn(), e); }
+
+/** \brief If-then-else for natural numbers */
+inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(Nat, c, t, e); }
+
+class environment;
+/** \brief Import Natural number library in the given environment (if it has not been imported already). */
+void import_natlib(environment & env);
+}
diff --git a/src/library/arith/numtype.h b/src/library/arith/numtype.h
new file mode 100644
index 000000000..a1582002d
--- /dev/null
+++ b/src/library/arith/numtype.h
@@ -0,0 +1,20 @@
+/*
+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 "expr.h"
+#include "value.h"
+
+namespace lean {
+/** \brief Base class for numeric types */
+class num_type_value : public type_value {
+    name m_unicode;
+public:
+    num_type_value(name const & n, name const & u):type_value(n), m_unicode(u) {}
+    virtual ~num_type_value() {}
+    virtual name get_unicode_name() const { return m_unicode; }
+};
+}
diff --git a/src/library/arith/reallib.cpp b/src/library/arith/reallib.cpp
new file mode 100644
index 000000000..ca0b0c702
--- /dev/null
+++ b/src/library/arith/reallib.cpp
@@ -0,0 +1,159 @@
+/*
+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 "reallib.h"
+#include "intlib.h"
+#include "natlib.h"
+#include "numtype.h"
+#include "abstract.h"
+#include "environment.h"
+
+namespace lean {
+class real_type_value : public num_type_value {
+public:
+    real_type_value():num_type_value("Real", "\u211D") /* ℝ */ {}
+};
+expr const Real = mk_value(*(new real_type_value()));
+expr mk_real_type() { return Real; }
+
+class real_value_value : public value {
+    mpq m_val;
+public:
+    real_value_value(mpq const & v):m_val(v) {}
+    virtual ~real_value_value() {}
+    virtual expr get_type() const { return Real; }
+    virtual name get_name() const { return name{"Real", "numeral"}; }
+    virtual bool operator==(value const & other) const {
+        real_value_value const * _other = dynamic_cast<real_value_value const*>(&other);
+        return _other && _other->m_val == m_val;
+    }
+    virtual void display(std::ostream & out) const { out << m_val; }
+    virtual format pp() const { return format(m_val); }
+    virtual format pp(bool unicode) const { return pp(); }
+    virtual unsigned hash() const { return m_val.hash(); }
+    mpq const & get_num() const { return m_val; }
+};
+
+expr mk_real_value(mpq const & v) {
+    return mk_value(*(new real_value_value(v)));
+}
+
+bool is_real_value(expr const & e) {
+    return is_value(e) && dynamic_cast<real_value_value const *>(&to_value(e)) != nullptr;
+}
+
+mpq const & real_value_numeral(expr const & e) {
+    lean_assert(is_real_value(e));
+    return static_cast<real_value_value const &>(to_value(e)).get_num();
+}
+
+template<char const * Name, typename F>
+class real_bin_op : public const_value {
+public:
+    real_bin_op():const_value(name("Real", Name), Real >> (Real >> Real)) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
+            r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2])));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+
+constexpr char real_add_name[] = "add";
+struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; };
+typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
+MK_BUILTIN(real_add_fn, real_add_value);
+
+constexpr char real_mul_name[] = "mul";
+struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; };
+typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
+MK_BUILTIN(real_mul_fn, real_mul_value);
+
+constexpr char real_div_name[] = "div";
+struct real_div_eval {
+    mpq operator()(mpq const & v1, mpq const & v2) {
+        if (v2.is_zero())
+            return v2;
+        else
+            return v1 / v2;
+    };
+};
+typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
+MK_BUILTIN(real_div_fn, real_div_value);
+
+class real_le_value : public const_value {
+public:
+    real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
+            r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2]));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+MK_BUILTIN(real_le_fn, real_le_value);
+
+MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
+MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
+MK_CONSTANT(real_abs_fn, name({"Real", "abs"}));
+MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
+MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
+MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
+
+void import_reallib(environment & env) {
+    if (env.find_object(to_value(Real).get_name()))
+        return;
+    expr rr_b = Real >> (Real >> Bool);
+    expr rr_r = Real >> (Real >> Real);
+    expr r_r  = Real >> Real;
+    expr x    = Const("x");
+    expr y    = Const("y");
+
+    env.add_builtin(Real);
+    env.add_builtin_set(rVal(0));
+    env.add_builtin(mk_real_add_fn());
+    env.add_builtin(mk_real_mul_fn());
+    env.add_builtin(mk_real_div_fn());
+    env.add_builtin(mk_real_le_fn());
+
+    env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y))));
+    env.add_definition(real_neg_fn_name, r_r,  Fun({x, Real}, rMul(rVal(-1), x)));
+    env.add_definition(real_abs_fn_name, r_r,  Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x))));
+    env.add_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));
+    env.add_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
+    env.add_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
+}
+
+class int_to_real_value : public const_value {
+public:
+    int_to_real_value():const_value("int_to_real", Int >> Real) {}
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 2 && is_int_value(args[1])) {
+            r = mk_real_value(mpq(int_value_numeral(args[1])));
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+MK_BUILTIN(int_to_real_fn,  int_to_real_value);
+MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
+
+void import_int_to_real_coercions(environment & env) {
+    if (env.find_object(to_value(mk_int_to_real_fn()).get_name()))
+        return;
+    import_intlib(env);
+    import_reallib(env);
+
+    env.add_builtin(mk_int_to_real_fn());
+    expr x    = Const("x");
+    env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
+}
+}
diff --git a/src/library/arith/reallib.h b/src/library/arith/reallib.h
new file mode 100644
index 000000000..0a24e37fd
--- /dev/null
+++ b/src/library/arith/reallib.h
@@ -0,0 +1,80 @@
+/*
+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 "expr.h"
+#include "builtin.h"
+#include "mpq.h"
+
+namespace lean {
+/** \brief Real numbers type */
+expr mk_real_type();
+extern expr const Real;
+
+/** \brief Return the value of type Real that represents \c v. */
+expr mk_real_value(mpq const & v);
+inline expr mk_real_value(int v) { return mk_real_value(mpq(v)); }
+inline expr rVal(int v) { return mk_real_value(v); }
+bool is_real_value(expr const & e);
+mpq const & real_value_numeral(expr const & e);
+
+/** \brief Addition, Real::add : Real -> Real -> Real */
+expr mk_real_add_fn();
+inline expr rAdd(expr const & e1, expr const & e2) { return mk_app(mk_real_add_fn(), e1, e2); }
+
+/** \brief Subtraction, Real::sub : Real -> Real -> Real */
+expr mk_real_sub_fn();
+inline expr rSub(expr const & e1, expr const & e2) { return mk_app(mk_real_sub_fn(), e1, e2); }
+
+/** \brief Unary minus, Real::neg : Real -> Real */
+expr mk_real_neg_fn();
+inline expr rNeg(expr const & e) { return mk_app(mk_real_neg_fn(), e); }
+
+/** \brief Multiplication, Real::mul : Real -> Real -> Real */
+expr mk_real_mul_fn();
+inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_fn(), e1, e2); }
+
+/** \brief Division, Real::mul : Real -> Real -> Real */
+expr mk_real_div_fn();
+inline expr rDiv(expr const & e1, expr const & e2) { return mk_app(mk_real_div_fn(), e1, e2); }
+
+/** \brief Absolute value function, Real::abs : Real -> Real */
+expr mk_real_abs_fn();
+inline expr rAbs(expr const & e) { return mk_app(mk_real_abs_fn(), e); }
+
+/** \brief Less than or equal to, Real::le : Real -> Real -> Bool */
+expr mk_real_le_fn();
+inline expr rLe(expr const & e1, expr const & e2) { return mk_app(mk_real_le_fn(), e1, e2); }
+
+/** \brief Greater than or equal to, Real::ge : Real -> Real -> Bool */
+expr mk_real_ge_fn();
+inline expr rGe(expr const & e1, expr const & e2) { return mk_app(mk_real_ge_fn(), e1, e2); }
+
+/** \brief Less than, Real::lt : Real -> Real -> Bool */
+expr mk_real_lt_fn();
+inline expr rLt(expr const & e1, expr const & e2) { return mk_app(mk_real_lt_fn(), e1, e2); }
+
+/** \brief Greater than, Real::gt : Real -> Real -> Bool */
+expr mk_real_gt_fn();
+inline expr rGt(expr const & e1, expr const & e2) { return mk_app(mk_real_gt_fn(), e1, e2); }
+
+/** \brief If-then-else for reals */
+inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(Real, c, t, e); }
+
+class environment;
+/** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */
+void import_reallib(environment & env);
+
+/** \brief Coercion from int to real */
+expr mk_int_to_real_fn();
+inline expr i2r(expr const & e) { return mk_app(mk_int_to_real_fn(), e); }
+/** \brief Coercion from nat to real */
+expr mk_nat_to_real_fn();
+inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); }
+
+/** \brief Import the coercions \c i2r and \c n2r. The Integer and (basic) Real libraries are also imported. */
+void import_int_to_real_coercions(environment & env);
+}
diff --git a/src/library/arith/specialfnlib.cpp b/src/library/arith/specialfnlib.cpp
new file mode 100644
index 000000000..ea985d6bc
--- /dev/null
+++ b/src/library/arith/specialfnlib.cpp
@@ -0,0 +1,60 @@
+/*
+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 "specialfnlib.h"
+#include "reallib.h"
+#include "abstract.h"
+#include "environment.h"
+
+namespace lean {
+MK_CONSTANT(exp_fn, name("exp"));
+MK_CONSTANT(log_fn, name("log"));
+
+MK_CONSTANT(real_pi, name("\u03C0")); // lower case pi
+MK_CONSTANT(sin_fn, name("sin"));
+MK_CONSTANT(cos_fn, name("cos"));
+MK_CONSTANT(tan_fn, name("tan"));
+MK_CONSTANT(cot_fn, name("cot"));
+MK_CONSTANT(sec_fn, name("sec"));
+MK_CONSTANT(csc_fn, name("csc"));
+
+MK_CONSTANT(sinh_fn, name("sinh"));
+MK_CONSTANT(cosh_fn, name("cosh"));
+MK_CONSTANT(tanh_fn, name("tanh"));
+MK_CONSTANT(coth_fn, name("coth"));
+MK_CONSTANT(sech_fn, name("sech"));
+MK_CONSTANT(csch_fn, name("csch"));
+
+void import_specialfnlib(environment & env) {
+    if (env.find_object(const_name(mk_exp_fn())))
+        return;
+    import_reallib(env);
+
+    expr r_r  = Real >> Real;
+    expr x    = Const("x");
+
+    env.add_var(exp_fn_name, r_r);
+    env.add_var(log_fn_name, r_r);
+
+    env.add_var(real_pi_name, Real);
+    env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
+    env.add_var(sin_fn_name, r_r);
+    env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
+    env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x))));
+    env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x))));
+    env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cos(x))));
+    env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sin(x))));
+
+    env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
+                                                              rMul(rVal(2), Exp(rNeg(x))))));
+    env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
+                                                              rMul(rVal(2), Exp(rNeg(x))))));
+    env.add_definition(tanh_fn_name, r_r, Fun({x,Real}, rDiv(Sinh(x), Cosh(x))));
+    env.add_definition(coth_fn_name, r_r, Fun({x,Real}, rDiv(Cosh(x), Sinh(x))));
+    env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cosh(x))));
+    env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sinh(x))));
+}
+}
diff --git a/src/library/arith/specialfnlib.h b/src/library/arith/specialfnlib.h
new file mode 100644
index 000000000..82c17df1c
--- /dev/null
+++ b/src/library/arith/specialfnlib.h
@@ -0,0 +1,63 @@
+/*
+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 "expr.h"
+
+namespace lean {
+// Special functions library
+
+expr mk_exp_fn();
+inline expr Exp(expr const & e) { return mk_app(mk_exp_fn(), e); }
+
+expr mk_log_fn();
+inline expr Log(expr const & e) { return mk_app(mk_log_fn(), e); }
+
+expr mk_real_pi();
+
+expr mk_sin_fn();
+inline expr Sin(expr const & e) { return mk_app(mk_sin_fn(), e); }
+
+expr mk_cos_fn();
+inline expr Cos(expr const & e) { return mk_app(mk_cos_fn(), e); }
+
+expr mk_tan_fn();
+inline expr Tan(expr const & e) { return mk_app(mk_tan_fn(), e); }
+
+expr mk_cot_fn();
+inline expr Cot(expr const & e) { return mk_app(mk_cot_fn(), e); }
+
+expr mk_sec_fn();
+inline expr Sec(expr const & e) { return mk_app(mk_sec_fn(), e); }
+
+expr mk_csc_fn();
+inline expr Csc(expr const & e) { return mk_app(mk_csc_fn(), e); }
+
+expr mk_sinh_fn();
+inline expr Sinh(expr const & e) { return mk_app(mk_sinh_fn(), e); }
+
+expr mk_cosh_fn();
+inline expr Cosh(expr const & e) { return mk_app(mk_cosh_fn(), e); }
+
+expr mk_tanh_fn();
+inline expr Tanh(expr const & e) { return mk_app(mk_tanh_fn(), e); }
+
+expr mk_coth_fn();
+inline expr Coth(expr const & e) { return mk_app(mk_coth_fn(), e); }
+
+expr mk_sech_fn();
+inline expr Sech(expr const & e) { return mk_app(mk_sech_fn(), e); }
+
+expr mk_csch_fn();
+inline expr Csch(expr const & e) { return mk_app(mk_csch_fn(), e); }
+
+class environment;
+/**
+    \brief Import the special function library (if it has not been imported already).
+    The (basic) Real Number library is also imported.
+*/
+void import_specialfnlib(environment & env);
+}
diff --git a/src/library/import_all/CMakeLists.txt b/src/library/import_all/CMakeLists.txt
new file mode 100644
index 000000000..f906d6eeb
--- /dev/null
+++ b/src/library/import_all/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_library(import_all import_all.cpp)
+target_link_libraries(import_all ${LEAN_LIBS})
diff --git a/src/library/toplevel.cpp b/src/library/import_all/import_all.cpp
similarity index 72%
rename from src/library/toplevel.cpp
rename to src/library/import_all/import_all.cpp
index 068ba79f2..83ddb81c3 100644
--- a/src/library/toplevel.cpp
+++ b/src/library/import_all/import_all.cpp
@@ -4,20 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "toplevel.h"
+#include "import_all.h"
 #include "builtin.h"
 #include "basic_thms.h"
-#include "arith.h"
+#include "arithlibs.h"
 
 namespace lean {
-void init_toplevel(environment & env) {
+void import_all(environment & env) {
     add_basic_theory(env);
     add_basic_thms(env);
-    add_arith_theory(env);
+    import_arithlibs(env);
 }
 environment mk_toplevel() {
     environment r;
-    init_toplevel(r);
+    import_all(r);
     return r;
 }
 }
diff --git a/src/library/toplevel.h b/src/library/import_all/import_all.h
similarity index 55%
rename from src/library/toplevel.h
rename to src/library/import_all/import_all.h
index 11a60f306..7668b2ed4 100644
--- a/src/library/toplevel.h
+++ b/src/library/import_all/import_all.h
@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include "environment.h"
 
 namespace lean {
-/** \brief Initialize environment with builtin objects and basic theorems. */
-void init_toplevel(environment & env);
-/** \brief Create top-level environment with builtin objects and basic theorems. */
+/** \brief Import all builtin libraries and theorems */
+void import_all(environment & env);
+/** \brief Create top-level environment with all builtin libraries and theorems */
 environment mk_toplevel();
 }
diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp
index c67df1f9a..9a9969f43 100644
--- a/src/tests/frontends/lean/implicit_args.cpp
+++ b/src/tests/frontends/lean/implicit_args.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "printer.h"
 #include "occurs.h"
 #include "abstract.h"
-#include "toplevel.h"
+#include "import_all.h"
 #include "basic_thms.h"
 #include "type_checker.h"
 #include "kernel_exception.h"
diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp
index aff086366..ef22ec829 100644
--- a/src/tests/kernel/arith.cpp
+++ b/src/tests/kernel/arith.cpp
@@ -8,9 +8,9 @@ Author: Leonardo de Moura
 #include "environment.h"
 #include "type_checker.h"
 #include "builtin.h"
-#include "arith.h"
+#include "arithlibs.h"
 #include "normalizer.h"
-#include "toplevel.h"
+#include "import_all.h"
 #include "abstract.h"
 #include "printer.h"
 #include "test.h"
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index ba597318e..bcebe5712 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -8,9 +8,9 @@ Author: Leonardo de Moura
 #include "environment.h"
 #include "type_checker.h"
 #include "printer.h"
-#include "toplevel.h"
+#include "import_all.h"
 #include "builtin.h"
-#include "arith.h"
+#include "arithlibs.h"
 #include "normalizer.h"
 #include "abstract.h"
 #include "exception.h"
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 95037738b..4ce817f51 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 #include "instantiate.h"
 #include "printer.h"
 #include "deep_copy.h"
-#include "arith.h"
+#include "arithlibs.h"
 using namespace lean;
 
 void tst1() {
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index a7a24969f..9e219d52b 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 #include "expr_sets.h"
 #include "abstract.h"
 #include "kernel_exception.h"
-#include "toplevel.h"
+#include "import_all.h"
 #include "printer.h"
 using namespace lean;
 
diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp
index 436d8919b..392dba177 100644
--- a/src/tests/kernel/threads.cpp
+++ b/src/tests/kernel/threads.cpp
@@ -13,8 +13,8 @@ Author: Leonardo de Moura
 #include "deep_copy.h"
 #include "abstract.h"
 #include "normalizer.h"
-#include "toplevel.h"
-#include "arith.h"
+#include "import_all.h"
+#include "arithlibs.h"
 #include "test.h"
 using namespace lean;
 
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 92eb3d77d..96b396532 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -11,10 +11,10 @@ Author: Leonardo de Moura
 #include "environment.h"
 #include "abstract.h"
 #include "exception.h"
-#include "toplevel.h"
+#include "import_all.h"
 #include "basic_thms.h"
 #include "builtin.h"
-#include "arith.h"
+#include "arithlibs.h"
 #include "normalizer.h"
 #include "printer.h"
 #include "trace.h"