diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 30efa3e40..ca71aa69e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -215,8 +215,6 @@ add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
 add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
-# add_subdirectory(library/arith)
-# set(LEAN_LIBS ${LEAN_LIBS} arithlib)
 # add_subdirectory(library/rewriter)
 # set(LEAN_LIBS ${LEAN_LIBS} rewriter)
 # add_subdirectory(library/simplifier)
diff --git a/src/library/arith/CMakeLists.txt b/src/library/arith/CMakeLists.txt
deleted file mode 100644
index 5bb7ae295..000000000
--- a/src/library/arith/CMakeLists.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-add_library(arithlib nat.cpp int.cpp real.cpp arith.cpp)
-target_link_libraries(arithlib ${LEAN_LIBS})
diff --git a/src/library/arith/Int_decls.cpp b/src/library/arith/Int_decls.cpp
deleted file mode 100644
index 53b120c91..000000000
--- a/src/library/arith/Int_decls.cpp
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-*/
-// Automatically generated file, DO NOT EDIT
-#include "kernel/environment.h"
-#include "kernel/decl_macros.h"
-namespace lean {
-MK_CONSTANT(Int, name("Int"));
-MK_CONSTANT(Int_ge_fn, name({"Int", "ge"}));
-MK_CONSTANT(Int_lt_fn, name({"Int", "lt"}));
-MK_CONSTANT(Int_gt_fn, name({"Int", "gt"}));
-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(Nat_sub_fn, name({"Nat", "sub"}));
-MK_CONSTANT(Nat_neg_fn, name({"Nat", "neg"}));
-}
diff --git a/src/library/arith/Int_decls.h b/src/library/arith/Int_decls.h
deleted file mode 100644
index 985a5bc20..000000000
--- a/src/library/arith/Int_decls.h
+++ /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.
-*/
-// Automatically generated file, DO NOT EDIT
-#include "kernel/expr.h"
-namespace lean {
-expr mk_Int();
-bool is_Int(expr const & e);
-expr mk_Int_ge_fn();
-bool is_Int_ge_fn(expr const & e);
-inline bool is_Int_ge(expr const & e) { return is_app(e) && is_Int_ge_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Int_ge(expr const & e1, expr const & e2) { return mk_app({mk_Int_ge_fn(), e1, e2}); }
-expr mk_Int_lt_fn();
-bool is_Int_lt_fn(expr const & e);
-inline bool is_Int_lt(expr const & e) { return is_app(e) && is_Int_lt_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Int_lt(expr const & e1, expr const & e2) { return mk_app({mk_Int_lt_fn(), e1, e2}); }
-expr mk_Int_gt_fn();
-bool is_Int_gt_fn(expr const & e);
-inline bool is_Int_gt(expr const & e) { return is_app(e) && is_Int_gt_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Int_gt(expr const & e1, expr const & e2) { return mk_app({mk_Int_gt_fn(), e1, e2}); }
-expr mk_Int_sub_fn();
-bool is_Int_sub_fn(expr const & e);
-inline bool is_Int_sub(expr const & e) { return is_app(e) && is_Int_sub_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Int_sub(expr const & e1, expr const & e2) { return mk_app({mk_Int_sub_fn(), e1, e2}); }
-expr mk_Int_neg_fn();
-bool is_Int_neg_fn(expr const & e);
-inline bool is_Int_neg(expr const & e) { return is_app(e) && is_Int_neg_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_Int_neg(expr const & e1) { return mk_app({mk_Int_neg_fn(), e1}); }
-expr mk_Int_mod_fn();
-bool is_Int_mod_fn(expr const & e);
-inline bool is_Int_mod(expr const & e) { return is_app(e) && is_Int_mod_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Int_mod(expr const & e1, expr const & e2) { return mk_app({mk_Int_mod_fn(), e1, e2}); }
-expr mk_Int_divides_fn();
-bool is_Int_divides_fn(expr const & e);
-inline bool is_Int_divides(expr const & e) { return is_app(e) && is_Int_divides_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Int_divides(expr const & e1, expr const & e2) { return mk_app({mk_Int_divides_fn(), e1, e2}); }
-expr mk_Int_abs_fn();
-bool is_Int_abs_fn(expr const & e);
-inline bool is_Int_abs(expr const & e) { return is_app(e) && is_Int_abs_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_Int_abs(expr const & e1) { return mk_app({mk_Int_abs_fn(), e1}); }
-expr mk_Nat_sub_fn();
-bool is_Nat_sub_fn(expr const & e);
-inline bool is_Nat_sub(expr const & e) { return is_app(e) && is_Nat_sub_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Nat_sub(expr const & e1, expr const & e2) { return mk_app({mk_Nat_sub_fn(), e1, e2}); }
-expr mk_Nat_neg_fn();
-bool is_Nat_neg_fn(expr const & e);
-inline bool is_Nat_neg(expr const & e) { return is_app(e) && is_Nat_neg_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_Nat_neg(expr const & e1) { return mk_app({mk_Nat_neg_fn(), e1}); }
-}
diff --git a/src/library/arith/Nat_decls.cpp b/src/library/arith/Nat_decls.cpp
deleted file mode 100644
index dc343031f..000000000
--- a/src/library/arith/Nat_decls.cpp
+++ /dev/null
@@ -1,60 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-*/
-// Automatically generated file, DO NOT EDIT
-#include "kernel/environment.h"
-#include "kernel/decl_macros.h"
-namespace lean {
-MK_CONSTANT(Nat, name("Nat"));
-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"}));
-MK_CONSTANT(Nat_succ_nz_fn, name({"Nat", "succ_nz"}));
-MK_CONSTANT(Nat_succ_inj_fn, name({"Nat", "succ_inj"}));
-MK_CONSTANT(Nat_add_zeror_fn, name({"Nat", "add_zeror"}));
-MK_CONSTANT(Nat_add_succr_fn, name({"Nat", "add_succr"}));
-MK_CONSTANT(Nat_mul_zeror_fn, name({"Nat", "mul_zeror"}));
-MK_CONSTANT(Nat_mul_succr_fn, name({"Nat", "mul_succr"}));
-MK_CONSTANT(Nat_le_def_fn, name({"Nat", "le_def"}));
-MK_CONSTANT(Nat_induction_fn, name({"Nat", "induction"}));
-MK_CONSTANT(Nat_induction_on_fn, name({"Nat", "induction_on"}));
-MK_CONSTANT(Nat_pred_nz_fn, name({"Nat", "pred_nz"}));
-MK_CONSTANT(Nat_discriminate_fn, name({"Nat", "discriminate"}));
-MK_CONSTANT(Nat_add_zerol_fn, name({"Nat", "add_zerol"}));
-MK_CONSTANT(Nat_add_succl_fn, name({"Nat", "add_succl"}));
-MK_CONSTANT(Nat_add_comm_fn, name({"Nat", "add_comm"}));
-MK_CONSTANT(Nat_add_assoc_fn, name({"Nat", "add_assoc"}));
-MK_CONSTANT(Nat_mul_zerol_fn, name({"Nat", "mul_zerol"}));
-MK_CONSTANT(Nat_mul_succl_fn, name({"Nat", "mul_succl"}));
-MK_CONSTANT(Nat_mul_onel_fn, name({"Nat", "mul_onel"}));
-MK_CONSTANT(Nat_mul_oner_fn, name({"Nat", "mul_oner"}));
-MK_CONSTANT(Nat_mul_comm_fn, name({"Nat", "mul_comm"}));
-MK_CONSTANT(Nat_distributer_fn, name({"Nat", "distributer"}));
-MK_CONSTANT(Nat_distributel_fn, name({"Nat", "distributel"}));
-MK_CONSTANT(Nat_mul_assoc_fn, name({"Nat", "mul_assoc"}));
-MK_CONSTANT(Nat_add_left_comm_fn, name({"Nat", "add_left_comm"}));
-MK_CONSTANT(Nat_mul_left_comm_fn, name({"Nat", "mul_left_comm"}));
-MK_CONSTANT(Nat_add_injr_fn, name({"Nat", "add_injr"}));
-MK_CONSTANT(Nat_add_injl_fn, name({"Nat", "add_injl"}));
-MK_CONSTANT(Nat_add_eqz_fn, name({"Nat", "add_eqz"}));
-MK_CONSTANT(Nat_le_intro_fn, name({"Nat", "le_intro"}));
-MK_CONSTANT(Nat_le_elim_fn, name({"Nat", "le_elim"}));
-MK_CONSTANT(Nat_le_refl_fn, name({"Nat", "le_refl"}));
-MK_CONSTANT(Nat_le_zero_fn, name({"Nat", "le_zero"}));
-MK_CONSTANT(Nat_le_trans_fn, name({"Nat", "le_trans"}));
-MK_CONSTANT(Nat_le_add_fn, name({"Nat", "le_add"}));
-MK_CONSTANT(Nat_le_antisym_fn, name({"Nat", "le_antisym"}));
-MK_CONSTANT(Nat_not_lt_0_fn, name({"Nat", "not_lt_0"}));
-MK_CONSTANT(Nat_lt_intro_fn, name({"Nat", "lt_intro"}));
-MK_CONSTANT(Nat_lt_elim_fn, name({"Nat", "lt_elim"}));
-MK_CONSTANT(Nat_lt_le_fn, name({"Nat", "lt_le"}));
-MK_CONSTANT(Nat_lt_ne_fn, name({"Nat", "lt_ne"}));
-MK_CONSTANT(Nat_lt_nrefl_fn, name({"Nat", "lt_nrefl"}));
-MK_CONSTANT(Nat_lt_trans_fn, name({"Nat", "lt_trans"}));
-MK_CONSTANT(Nat_lt_le_trans_fn, name({"Nat", "lt_le_trans"}));
-MK_CONSTANT(Nat_le_lt_trans_fn, name({"Nat", "le_lt_trans"}));
-MK_CONSTANT(Nat_ne_lt_succ_fn, name({"Nat", "ne_lt_succ"}));
-MK_CONSTANT(Nat_strong_induction_fn, name({"Nat", "strong_induction"}));
-}
diff --git a/src/library/arith/Nat_decls.h b/src/library/arith/Nat_decls.h
deleted file mode 100644
index ee5cedf27..000000000
--- a/src/library/arith/Nat_decls.h
+++ /dev/null
@@ -1,164 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-*/
-// Automatically generated file, DO NOT EDIT
-#include "kernel/expr.h"
-namespace lean {
-expr mk_Nat();
-bool is_Nat(expr const & e);
-expr mk_Nat_ge_fn();
-bool is_Nat_ge_fn(expr const & e);
-inline bool is_Nat_ge(expr const & e) { return is_app(e) && is_Nat_ge_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Nat_ge(expr const & e1, expr const & e2) { return mk_app({mk_Nat_ge_fn(), e1, e2}); }
-expr mk_Nat_lt_fn();
-bool is_Nat_lt_fn(expr const & e);
-inline bool is_Nat_lt(expr const & e) { return is_app(e) && is_Nat_lt_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Nat_lt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_lt_fn(), e1, e2}); }
-expr mk_Nat_gt_fn();
-bool is_Nat_gt_fn(expr const & e);
-inline bool is_Nat_gt(expr const & e) { return is_app(e) && is_Nat_gt_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Nat_gt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_gt_fn(), e1, e2}); }
-expr mk_Nat_id_fn();
-bool is_Nat_id_fn(expr const & e);
-inline bool is_Nat_id(expr const & e) { return is_app(e) && is_Nat_id_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_Nat_id(expr const & e1) { return mk_app({mk_Nat_id_fn(), e1}); }
-expr mk_Nat_succ_nz_fn();
-bool is_Nat_succ_nz_fn(expr const & e);
-inline expr mk_Nat_succ_nz_th(expr const & e1) { return mk_app({mk_Nat_succ_nz_fn(), e1}); }
-expr mk_Nat_succ_inj_fn();
-bool is_Nat_succ_inj_fn(expr const & e);
-inline expr mk_Nat_succ_inj_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_succ_inj_fn(), e1, e2, e3}); }
-expr mk_Nat_add_zeror_fn();
-bool is_Nat_add_zeror_fn(expr const & e);
-inline expr mk_Nat_add_zeror_th(expr const & e1) { return mk_app({mk_Nat_add_zeror_fn(), e1}); }
-expr mk_Nat_add_succr_fn();
-bool is_Nat_add_succr_fn(expr const & e);
-inline expr mk_Nat_add_succr_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_succr_fn(), e1, e2}); }
-expr mk_Nat_mul_zeror_fn();
-bool is_Nat_mul_zeror_fn(expr const & e);
-inline expr mk_Nat_mul_zeror_th(expr const & e1) { return mk_app({mk_Nat_mul_zeror_fn(), e1}); }
-expr mk_Nat_mul_succr_fn();
-bool is_Nat_mul_succr_fn(expr const & e);
-inline expr mk_Nat_mul_succr_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_succr_fn(), e1, e2}); }
-expr mk_Nat_le_def_fn();
-bool is_Nat_le_def_fn(expr const & e);
-inline expr mk_Nat_le_def_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_le_def_fn(), e1, e2}); }
-expr mk_Nat_induction_fn();
-bool is_Nat_induction_fn(expr const & e);
-inline expr mk_Nat_induction_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_induction_on_fn();
-bool is_Nat_induction_on_fn(expr const & e);
-inline expr mk_Nat_induction_on_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_on_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_pred_nz_fn();
-bool is_Nat_pred_nz_fn(expr const & e);
-inline expr mk_Nat_pred_nz_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_pred_nz_fn(), e1, e2}); }
-expr mk_Nat_discriminate_fn();
-bool is_Nat_discriminate_fn(expr const & e);
-inline expr mk_Nat_discriminate_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_discriminate_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_add_zerol_fn();
-bool is_Nat_add_zerol_fn(expr const & e);
-inline expr mk_Nat_add_zerol_th(expr const & e1) { return mk_app({mk_Nat_add_zerol_fn(), e1}); }
-expr mk_Nat_add_succl_fn();
-bool is_Nat_add_succl_fn(expr const & e);
-inline expr mk_Nat_add_succl_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_succl_fn(), e1, e2}); }
-expr mk_Nat_add_comm_fn();
-bool is_Nat_add_comm_fn(expr const & e);
-inline expr mk_Nat_add_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_comm_fn(), e1, e2}); }
-expr mk_Nat_add_assoc_fn();
-bool is_Nat_add_assoc_fn(expr const & e);
-inline expr mk_Nat_add_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_assoc_fn(), e1, e2, e3}); }
-expr mk_Nat_mul_zerol_fn();
-bool is_Nat_mul_zerol_fn(expr const & e);
-inline expr mk_Nat_mul_zerol_th(expr const & e1) { return mk_app({mk_Nat_mul_zerol_fn(), e1}); }
-expr mk_Nat_mul_succl_fn();
-bool is_Nat_mul_succl_fn(expr const & e);
-inline expr mk_Nat_mul_succl_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_succl_fn(), e1, e2}); }
-expr mk_Nat_mul_onel_fn();
-bool is_Nat_mul_onel_fn(expr const & e);
-inline expr mk_Nat_mul_onel_th(expr const & e1) { return mk_app({mk_Nat_mul_onel_fn(), e1}); }
-expr mk_Nat_mul_oner_fn();
-bool is_Nat_mul_oner_fn(expr const & e);
-inline expr mk_Nat_mul_oner_th(expr const & e1) { return mk_app({mk_Nat_mul_oner_fn(), e1}); }
-expr mk_Nat_mul_comm_fn();
-bool is_Nat_mul_comm_fn(expr const & e);
-inline expr mk_Nat_mul_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_comm_fn(), e1, e2}); }
-expr mk_Nat_distributer_fn();
-bool is_Nat_distributer_fn(expr const & e);
-inline expr mk_Nat_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_distributer_fn(), e1, e2, e3}); }
-expr mk_Nat_distributel_fn();
-bool is_Nat_distributel_fn(expr const & e);
-inline expr mk_Nat_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_distributel_fn(), e1, e2, e3}); }
-expr mk_Nat_mul_assoc_fn();
-bool is_Nat_mul_assoc_fn(expr const & e);
-inline expr mk_Nat_mul_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_assoc_fn(), e1, e2, e3}); }
-expr mk_Nat_add_left_comm_fn();
-bool is_Nat_add_left_comm_fn(expr const & e);
-inline expr mk_Nat_add_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_left_comm_fn(), e1, e2, e3}); }
-expr mk_Nat_mul_left_comm_fn();
-bool is_Nat_mul_left_comm_fn(expr const & e);
-inline expr mk_Nat_mul_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_left_comm_fn(), e1, e2, e3}); }
-expr mk_Nat_add_injr_fn();
-bool is_Nat_add_injr_fn(expr const & e);
-inline expr mk_Nat_add_injr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injr_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_add_injl_fn();
-bool is_Nat_add_injl_fn(expr const & e);
-inline expr mk_Nat_add_injl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injl_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_add_eqz_fn();
-bool is_Nat_add_eqz_fn(expr const & e);
-inline expr mk_Nat_add_eqz_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_eqz_fn(), e1, e2, e3}); }
-expr mk_Nat_le_intro_fn();
-bool is_Nat_le_intro_fn(expr const & e);
-inline expr mk_Nat_le_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_intro_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_le_elim_fn();
-bool is_Nat_le_elim_fn(expr const & e);
-inline expr mk_Nat_le_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_le_elim_fn(), e1, e2, e3}); }
-expr mk_Nat_le_refl_fn();
-bool is_Nat_le_refl_fn(expr const & e);
-inline expr mk_Nat_le_refl_th(expr const & e1) { return mk_app({mk_Nat_le_refl_fn(), e1}); }
-expr mk_Nat_le_zero_fn();
-bool is_Nat_le_zero_fn(expr const & e);
-inline expr mk_Nat_le_zero_th(expr const & e1) { return mk_app({mk_Nat_le_zero_fn(), e1}); }
-expr mk_Nat_le_trans_fn();
-bool is_Nat_le_trans_fn(expr const & e);
-inline expr mk_Nat_le_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_le_trans_fn(), e1, e2, e3, e4, e5}); }
-expr mk_Nat_le_add_fn();
-bool is_Nat_le_add_fn(expr const & e);
-inline expr mk_Nat_le_add_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_add_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_le_antisym_fn();
-bool is_Nat_le_antisym_fn(expr const & e);
-inline expr mk_Nat_le_antisym_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_antisym_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_not_lt_0_fn();
-bool is_Nat_not_lt_0_fn(expr const & e);
-inline expr mk_Nat_not_lt_0_th(expr const & e1) { return mk_app({mk_Nat_not_lt_0_fn(), e1}); }
-expr mk_Nat_lt_intro_fn();
-bool is_Nat_lt_intro_fn(expr const & e);
-inline expr mk_Nat_lt_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_lt_intro_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_lt_elim_fn();
-bool is_Nat_lt_elim_fn(expr const & e);
-inline expr mk_Nat_lt_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_elim_fn(), e1, e2, e3}); }
-expr mk_Nat_lt_le_fn();
-bool is_Nat_lt_le_fn(expr const & e);
-inline expr mk_Nat_lt_le_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_le_fn(), e1, e2, e3}); }
-expr mk_Nat_lt_ne_fn();
-bool is_Nat_lt_ne_fn(expr const & e);
-inline expr mk_Nat_lt_ne_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_ne_fn(), e1, e2, e3}); }
-expr mk_Nat_lt_nrefl_fn();
-bool is_Nat_lt_nrefl_fn(expr const & e);
-inline expr mk_Nat_lt_nrefl_th(expr const & e1) { return mk_app({mk_Nat_lt_nrefl_fn(), e1}); }
-expr mk_Nat_lt_trans_fn();
-bool is_Nat_lt_trans_fn(expr const & e);
-inline expr mk_Nat_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_trans_fn(), e1, e2, e3, e4, e5}); }
-expr mk_Nat_lt_le_trans_fn();
-bool is_Nat_lt_le_trans_fn(expr const & e);
-inline expr mk_Nat_lt_le_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_le_trans_fn(), e1, e2, e3, e4, e5}); }
-expr mk_Nat_le_lt_trans_fn();
-bool is_Nat_le_lt_trans_fn(expr const & e);
-inline expr mk_Nat_le_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_le_lt_trans_fn(), e1, e2, e3, e4, e5}); }
-expr mk_Nat_ne_lt_succ_fn();
-bool is_Nat_ne_lt_succ_fn(expr const & e);
-inline expr mk_Nat_ne_lt_succ_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_ne_lt_succ_fn(), e1, e2, e3, e4}); }
-expr mk_Nat_strong_induction_fn();
-bool is_Nat_strong_induction_fn(expr const & e);
-inline expr mk_Nat_strong_induction_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_strong_induction_fn(), e1, e2, e3}); }
-}
diff --git a/src/library/arith/Real_decls.cpp b/src/library/arith/Real_decls.cpp
deleted file mode 100644
index e4b8f173c..000000000
--- a/src/library/arith/Real_decls.cpp
+++ /dev/null
@@ -1,17 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-*/
-// Automatically generated file, DO NOT EDIT
-#include "kernel/environment.h"
-#include "kernel/decl_macros.h"
-namespace lean {
-MK_CONSTANT(Real, name("Real"));
-MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
-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(Real_sub_fn, name({"Real", "sub"}));
-MK_CONSTANT(Real_neg_fn, name({"Real", "neg"}));
-MK_CONSTANT(Real_abs_fn, name({"Real", "abs"}));
-}
diff --git a/src/library/arith/Real_decls.h b/src/library/arith/Real_decls.h
deleted file mode 100644
index 23c2a705d..000000000
--- a/src/library/arith/Real_decls.h
+++ /dev/null
@@ -1,38 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-*/
-// Automatically generated file, DO NOT EDIT
-#include "kernel/expr.h"
-namespace lean {
-expr mk_Real();
-bool is_Real(expr const & e);
-expr mk_nat_to_real_fn();
-bool is_nat_to_real_fn(expr const & e);
-inline bool is_nat_to_real(expr const & e) { return is_app(e) && is_nat_to_real_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_nat_to_real(expr const & e1) { return mk_app({mk_nat_to_real_fn(), e1}); }
-expr mk_Real_ge_fn();
-bool is_Real_ge_fn(expr const & e);
-inline bool is_Real_ge(expr const & e) { return is_app(e) && is_Real_ge_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Real_ge(expr const & e1, expr const & e2) { return mk_app({mk_Real_ge_fn(), e1, e2}); }
-expr mk_Real_lt_fn();
-bool is_Real_lt_fn(expr const & e);
-inline bool is_Real_lt(expr const & e) { return is_app(e) && is_Real_lt_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Real_lt(expr const & e1, expr const & e2) { return mk_app({mk_Real_lt_fn(), e1, e2}); }
-expr mk_Real_gt_fn();
-bool is_Real_gt_fn(expr const & e);
-inline bool is_Real_gt(expr const & e) { return is_app(e) && is_Real_gt_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Real_gt(expr const & e1, expr const & e2) { return mk_app({mk_Real_gt_fn(), e1, e2}); }
-expr mk_Real_sub_fn();
-bool is_Real_sub_fn(expr const & e);
-inline bool is_Real_sub(expr const & e) { return is_app(e) && is_Real_sub_fn(arg(e, 0)) && num_args(e) == 3; }
-inline expr mk_Real_sub(expr const & e1, expr const & e2) { return mk_app({mk_Real_sub_fn(), e1, e2}); }
-expr mk_Real_neg_fn();
-bool is_Real_neg_fn(expr const & e);
-inline bool is_Real_neg(expr const & e) { return is_app(e) && is_Real_neg_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_Real_neg(expr const & e1) { return mk_app({mk_Real_neg_fn(), e1}); }
-expr mk_Real_abs_fn();
-bool is_Real_abs_fn(expr const & e);
-inline bool is_Real_abs(expr const & e) { return is_app(e) && is_Real_abs_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_Real_abs(expr const & e1) { return mk_app({mk_Real_abs_fn(), e1}); }
-}
diff --git a/src/library/arith/arith.cpp b/src/library/arith/arith.cpp
deleted file mode 100644
index 25b41289f..000000000
--- a/src/library/arith/arith.cpp
+++ /dev/null
@@ -1,15 +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 "library/arith/arith.h"
-
-namespace lean {
-void import_arith(environment const & env, io_state const & ios) {
-    import_nat(env, ios);
-    import_int(env, ios);
-    import_real(env, ios);
-}
-}
diff --git a/src/library/arith/arith.h b/src/library/arith/arith.h
deleted file mode 100644
index d214fa75a..000000000
--- a/src/library/arith/arith.h
+++ /dev/null
@@ -1,18 +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 "library/arith/nat.h"
-#include "library/arith/int.h"
-#include "library/arith/real.h"
-
-namespace lean {
-class environment;
-/**
-   \brief Import all arithmetic related builtin libraries.
-*/
-void import_arith(environment const & env, io_state const & ios);
-}
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
deleted file mode 100644
index 2f3f98b46..000000000
--- a/src/library/arith/int.cpp
+++ /dev/null
@@ -1,162 +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 <string>
-#include "kernel/abstract.h"
-#include "kernel/environment.h"
-#include "kernel/value.h"
-#include "kernel/io_state.h"
-#include "kernel/decl_macros.h"
-#include "library/kernel_bindings.h"
-#include "library/arith/int.h"
-#include "library/arith/nat.h"
-#include "library/arith/Int_decls.cpp"
-
-namespace lean {
-expr mk_nat_to_int_fn();
-
-expr const Int = mk_Int();
-expr mk_int_type() { return mk_Int(); }
-
-class int_value_value : public value {
-    mpz m_val;
-protected:
-    virtual bool lt(value const & other) const {
-        return m_val < static_cast<int_value_value const &>(other).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 pp(false, false); }
-    virtual format pp(bool unicode, bool coercion) const {
-        if (coercion && m_val >= 0)
-            return format{to_value(mk_nat_to_int_fn()).pp(unicode, coercion), space(), format(m_val)};
-        else
-            return format(m_val);
-    }
-    virtual bool is_atomic_pp(bool /* unicode */, bool coercion) const { return !coercion || m_val < 0; }
-    virtual unsigned hash() const { return m_val.hash(); }
-    virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); }
-    mpz const & get_num() const { return m_val; }
-    virtual void write(serializer & s) const { s << "int" << m_val; }
-};
-
-expr mk_int_value(mpz const & v) {
-    return mk_value(*(new int_value_value(v)));
-}
-static value::register_deserializer_fn int_value_ds("int", [](deserializer & d) { return mk_int_value(read_mpz(d)); });
-static register_builtin_fn int_value_blt(name({"Int", "numeral"}), []() { return mk_int_value(mpz(0)); }, true);
-
-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();
-}
-
-/**
-   \brief Template for semantic attachments that are binary operators of
-   the form Int -> Int -> Int
-*/
-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 optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
-            return some_expr(mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2]))));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << (std::string("int_") + Name); }
-};
-
-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);
-static value::register_deserializer_fn int_add_ds("int_add", [](deserializer & ) { return mk_Int_add_fn(); });
-static register_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_Int_add_fn(); });
-
-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);
-static value::register_deserializer_fn int_mul_ds("int_mul", [](deserializer & ) { return mk_Int_mul_fn(); });
-static register_builtin_fn int_mul_blt(name({"Int", "mul"}), []() { return mk_Int_mul_fn(); });
-
-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);
-static value::register_deserializer_fn int_div_ds("int_div", [](deserializer & ) { return mk_Int_div_fn(); });
-static register_builtin_fn int_div_blt(name({"Int", "div"}), []() { return mk_Int_div_fn(); });
-
-class int_le_value : public const_value {
-public:
-    int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
-    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
-            return some_expr(mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2])));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << "int_le"; }
-};
-MK_BUILTIN(Int_le_fn, int_le_value);
-static value::register_deserializer_fn int_le_ds("int_le", [](deserializer & ) { return mk_Int_le_fn(); });
-static register_builtin_fn int_le_blt(name({"Int", "le"}), []() { return mk_Int_le_fn(); });
-
-/**
-   \brief Semantic attachment for the Nat to Int coercion.
-*/
-class nat_to_int_value : public const_value {
-public:
-    nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
-    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 2 && is_nat_value(args[1])) {
-            return some_expr(mk_int_value(nat_value_numeral(args[1])));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << "nat_to_int"; }
-};
-MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
-static value::register_deserializer_fn nat_to_int_ds("nat_to_int", [](deserializer & ) { return mk_nat_to_int_fn(); });
-static register_builtin_fn nat_to_int_blt("nat_to_int", []() { return mk_nat_to_int_fn(); });
-
-void import_int(environment const & env, io_state const & ios) {
-    env->import("Int", ios);
-}
-
-static int mk_int_value(lua_State * L) {
-    return push_expr(L, mk_int_value(to_mpz_ext(L, 1)));
-}
-
-void open_int(lua_State * L) {
-    SET_GLOBAL_FUN(mk_int_value,     "mk_int_value");
-    SET_GLOBAL_FUN(mk_int_value,     "iVal");
-}
-}
diff --git a/src/library/arith/int.h b/src/library/arith/int.h
deleted file mode 100644
index e114ed1ad..000000000
--- a/src/library/arith/int.h
+++ /dev/null
@@ -1,45 +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 "util/lua.h"
-#include "util/numerics/mpz.h"
-#include "kernel/expr.h"
-#include "kernel/kernel.h"
-#include "library/arith/Int_decls.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);
-
-expr mk_Int_add_fn();
-inline expr mk_Int_add(expr const & e1, expr const & e2) { return mk_app(mk_Int_add_fn(), e1, e2); }
-expr mk_Int_mul_fn();
-inline expr mk_Int_mul(expr const & e1, expr const & e2) { return mk_app(mk_Int_mul_fn(), e1, e2); }
-expr mk_Int_div_fn();
-inline expr mk_Int_div(expr const & e1, expr const & e2) { return mk_app(mk_Int_div_fn(), e1, e2); }
-expr mk_Int_le_fn();
-inline expr mk_Int_le(expr const & e1, expr const & e2) { return mk_app(mk_Int_le_fn(), e1, e2); }
-expr mk_nat_to_int_fn();
-inline expr mk_nat_to_int(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
-
-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_int(environment const & env, io_state const & ios);
-
-void open_int(lua_State * L);
-}
diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp
deleted file mode 100644
index ec575c418..000000000
--- a/src/library/arith/nat.cpp
+++ /dev/null
@@ -1,129 +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 <string>
-#include "kernel/abstract.h"
-#include "kernel/environment.h"
-#include "kernel/value.h"
-#include "kernel/io_state.h"
-#include "kernel/decl_macros.h"
-#include "library/kernel_bindings.h"
-#include "library/arith/nat.h"
-#include "library/arith/Nat_decls.cpp"
-
-namespace lean {
-expr const Nat = mk_Nat();
-expr mk_nat_type() { return mk_Nat(); }
-
-class nat_value_value : public value {
-    mpz m_val;
-protected:
-    virtual bool lt(value const & other) const {
-        return m_val < static_cast<nat_value_value const &>(other).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, bool) const { return pp(); }
-    virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return true; } // NOLINT
-    virtual unsigned hash() const { return m_val.hash(); }
-    virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); }
-    mpz const & get_num() const { return m_val; }
-    virtual void write(serializer & s) const { s << "nat" << m_val; }
-};
-expr mk_nat_value(mpz const & v) {
-    return mk_value(*(new nat_value_value(v)));
-}
-static value::register_deserializer_fn nat_value_ds("nat", [](deserializer & d) { return mk_nat_value(read_mpz(d)); });
-static register_builtin_fn nat_value_blt(name({"Nat", "numeral"}), []() { return mk_nat_value(mpz(0)); }, true);
-
-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();
-}
-
-/**
-   \brief Template for semantic attachments that are binary operators of
-   the form Nat -> Nat -> Nat
-*/
-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 optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
-            return some_expr(mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2]))));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << (std::string("nat_") + Name); }
-};
-
-constexpr char nat_add_name[] = "add";
-/** \brief Evaluator for + : Nat -> Nat -> Nat */
-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);
-static value::register_deserializer_fn nat_add_ds("nat_add", [](deserializer & ) { return mk_Nat_add_fn(); });
-static register_builtin_fn nat_add_blt(name({"Nat", "add"}), []() { return mk_Nat_add_fn(); });
-
-constexpr char nat_mul_name[] = "mul";
-/** \brief Evaluator for * : Nat -> Nat -> Nat */
-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);
-static value::register_deserializer_fn nat_mul_ds("nat_mul", [](deserializer & ) { return mk_Nat_mul_fn(); });
-static register_builtin_fn nat_mul_blt(name({"Nat", "mul"}), []() { return mk_Nat_mul_fn(); });
-
-/**
-   \brief Semantic attachment for less than or equal to operator with type
-   <code>Nat -> Nat -> Bool</code>
-*/
-class nat_le_value : public const_value {
-public:
-    nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
-    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
-            return some_expr(mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2])));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << "nat_le"; }
-};
-MK_BUILTIN(Nat_le_fn, nat_le_value);
-static value::register_deserializer_fn nat_le_ds("nat_le", [](deserializer & ) { return mk_Nat_le_fn(); });
-static register_builtin_fn nat_le_blt(name({"Nat", "le"}), []() { return mk_Nat_le_fn(); });
-
-void import_nat(environment const & env, io_state const & ios) {
-    env->import("Nat", ios);
-}
-
-static int mk_nat_value(lua_State * L) {
-    mpz v = to_mpz_ext(L, 1);
-    if (v < 0)
-        throw exception("arg #1 must be non-negative");
-    return push_expr(L, mk_nat_value(v));
-}
-
-void open_nat(lua_State * L) {
-    SET_GLOBAL_FUN(mk_nat_value,     "mk_nat_value");
-    SET_GLOBAL_FUN(mk_nat_value,     "nVal");
-}
-}
diff --git a/src/library/arith/nat.h b/src/library/arith/nat.h
deleted file mode 100644
index d12b11c33..000000000
--- a/src/library/arith/nat.h
+++ /dev/null
@@ -1,38 +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 "util/lua.h"
-#include "kernel/expr.h"
-#include "kernel/kernel.h"
-#include "util/numerics/mpz.h"
-#include "library/arith/Nat_decls.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);
-
-expr mk_Nat_add_fn();
-inline expr mk_Nat_add(expr const & e1, expr const & e2) { return mk_app(mk_Nat_add_fn(), e1, e2); }
-expr mk_Nat_mul_fn();
-inline expr mk_Nat_mul(expr const & e1, expr const & e2) { return mk_app(mk_Nat_mul_fn(), e1, e2); }
-expr mk_Nat_le_fn();
-inline expr mk_Nat_le(expr const & e1, expr const & e2) { return mk_app(mk_Nat_le_fn(), e1, e2); }
-
-class environment;
-/** \brief Import Natural number library in the given environment (if it has not been imported already). */
-void import_nat(environment const & env, io_state const & ios);
-
-void open_nat(lua_State * L);
-}
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
deleted file mode 100644
index 0ff87f0e2..000000000
--- a/src/library/arith/real.cpp
+++ /dev/null
@@ -1,165 +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 <string>
-#include "kernel/abstract.h"
-#include "kernel/environment.h"
-#include "kernel/value.h"
-#include "kernel/io_state.h"
-#include "kernel/decl_macros.h"
-#include "library/kernel_bindings.h"
-#include "library/arith/real.h"
-#include "library/arith/int.h"
-#include "library/arith/nat.h"
-#include "library/arith/Real_decls.cpp"
-
-namespace lean {
-expr const Real = mk_Real();
-expr mk_real_type() { return mk_Real(); }
-
-/**
-   \brief Semantic attachment for "Real" values.
-   It is actually for rational values. We should eventually rename it to
-   rat_value_value
-*/
-class real_value_value : public value {
-    mpq m_val;
-protected:
-    virtual bool lt(value const & other) const {
-        return m_val < static_cast<real_value_value const &>(other).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 pp(false, false); }
-    virtual format pp(bool, bool coercion) const {
-        if (coercion)
-            return format{format(const_name(mk_nat_to_real_fn())), space(), format(m_val)};
-        else
-            return format(m_val);
-    }
-    virtual bool is_atomic_pp(bool /* unicode */, bool coercion) const { return !coercion; }
-    virtual unsigned hash() const { return m_val.hash(); }
-    virtual int push_lua(lua_State * L) const { return push_mpq(L, m_val); }
-    mpq const & get_num() const { return m_val; }
-    virtual void write(serializer & s) const { s << "real" << 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();
-}
-static value::register_deserializer_fn real_value_ds("real", [](deserializer & d) { return mk_real_value(read_mpq(d)); });
-static register_builtin_fn real_value_blt(name({"Real", "numeral"}), []() { return mk_real_value(mpq(0)); }, true);
-
-/**
-   \brief Template for semantic attachments that are binary operators of
-   the form Real -> Real -> Real
-*/
-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 optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
-            return some_expr(mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2]))));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << (std::string("real_") + Name); }
-};
-
-constexpr char real_add_name[] = "add";
-/** \brief Evaluator for + : Real -> Real -> Real */
-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);
-static value::register_deserializer_fn real_add_ds("real_add", [](deserializer & ) { return mk_Real_add_fn(); });
-static register_builtin_fn real_add_blt(name({"Real", "add"}), []() { return mk_Real_add_fn(); });
-
-
-constexpr char real_mul_name[] = "mul";
-/** \brief Evaluator for * : Real -> Real -> Real */
-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);
-static value::register_deserializer_fn real_mul_ds("real_mul", [](deserializer & ) { return mk_Real_mul_fn(); });
-static register_builtin_fn real_mul_blt(name({"Real", "mul"}), []() { return mk_Real_mul_fn(); });
-
-constexpr char real_div_name[] = "div";
-/** \brief Evaluator for / : Real -> Real -> Real */
-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);
-static value::register_deserializer_fn real_div_ds("real_div", [](deserializer & ) { return mk_Real_div_fn(); });
-static register_builtin_fn real_div_blt(name({"Real", "div"}), []() { return mk_Real_div_fn(); });
-
-/**
-   \brief Semantic attachment for less than or equal to operator with type
-   <code>Real -> Real -> Bool</code>
-*/
-class real_le_value : public const_value {
-public:
-    real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
-    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
-            return some_expr(mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2])));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << "real_le"; }
-};
-MK_BUILTIN(Real_le_fn, real_le_value);
-static value::register_deserializer_fn real_le_ds("real_le", [](deserializer & ) { return mk_Real_le_fn(); });
-static register_builtin_fn real_le_btl(name({"Real", "le"}), []() { return mk_Real_le_fn(); });
-
-class int_to_real_value : public const_value {
-public:
-    int_to_real_value():const_value("int_to_real", Int >> Real) {}
-    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 2 && is_int_value(args[1])) {
-            return some_expr(mk_real_value(mpq(int_value_numeral(args[1]))));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << "int_to_real"; }
-};
-MK_BUILTIN(int_to_real_fn,  int_to_real_value);
-static value::register_deserializer_fn int_to_real_ds("int_to_real", [](deserializer & ) { return mk_int_to_real_fn(); });
-static register_builtin_fn int_to_real_blt("int_to_real", []() { return mk_int_to_real_fn(); });
-
-void import_real(environment const & env, io_state const & ios) {
-    env->import("Real", ios);
-}
-
-static int mk_real_value(lua_State * L) {
-    return push_expr(L, mk_real_value(to_mpq_ext(L, 1)));
-}
-
-void open_real(lua_State * L) {
-    SET_GLOBAL_FUN(mk_real_value,    "mk_real_value");
-    SET_GLOBAL_FUN(mk_real_value,    "rVal");
-}
-}
diff --git a/src/library/arith/real.h b/src/library/arith/real.h
deleted file mode 100644
index 6d3f95350..000000000
--- a/src/library/arith/real.h
+++ /dev/null
@@ -1,47 +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 "util/lua.h"
-#include "util/numerics/mpq.h"
-#include "kernel/expr.h"
-#include "kernel/kernel.h"
-#include "library/arith/Real_decls.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);
-
-expr mk_Real_add_fn();
-inline expr mk_Real_add(expr const & e1, expr const & e2) { return mk_app(mk_Real_add_fn(), e1, e2); }
-expr mk_Real_mul_fn();
-inline expr mk_Real_mul(expr const & e1, expr const & e2) { return mk_app(mk_Real_mul_fn(), e1, e2); }
-expr mk_Real_div_fn();
-inline expr mk_Real_div(expr const & e1, expr const & e2) { return mk_app(mk_Real_div_fn(), e1, e2); }
-expr mk_Real_le_fn();
-inline expr mk_Real_le(expr const & e1, expr const & e2) { return mk_app(mk_Real_le_fn(), e1, e2); }
-
-class environment;
-/** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */
-void import_real(environment const & env, io_state const & ios);
-
-/** \brief Coercion from int to real */
-expr mk_int_to_real_fn();
-inline expr mk_int_to_real(expr const & e) { return mk_app(mk_int_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 const & env);
-
-void open_real(lua_State * L);
-}
diff --git a/src/library/arith/register_module.h b/src/library/arith/register_module.h
deleted file mode 100644
index c68d9b705..000000000
--- a/src/library/arith/register_module.h
+++ /dev/null
@@ -1,22 +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 "util/script_state.h"
-#include "library/arith/nat.h"
-#include "library/arith/int.h"
-#include "library/arith/real.h"
-
-namespace lean {
-inline void open_arith_module(lua_State * L) {
-    open_nat(L);
-    open_int(L);
-    open_real(L);
-}
-inline void register_arith_module() {
-    script_state::register_module(open_arith_module);
-}
-}
diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp
deleted file mode 100644
index f1b2f43fa..000000000
--- a/src/tests/library/arith.cpp
+++ /dev/null
@@ -1,118 +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 "util/thread.h"
-#include "util/test.h"
-#include "kernel/kernel.h"
-#include "kernel/normalizer.h"
-#include "kernel/type_checker.h"
-#include "kernel/abstract.h"
-#include "library/io_state_stream.h"
-#include "library/arith/arith.h"
-#include "frontends/lean/frontend.h"
-#include "frontends/lua/register_modules.h"
-using namespace lean;
-
-static void tst0() {
-    environment env;
-    init_test_frontend(env);
-    normalizer  norm(env);
-    env->add_var("n", Nat);
-    expr n = Const("n");
-    lean_assert_eq(mk_nat_type(), Nat);
-    env->add_var("x", Real);
-    expr x = Const("x");
-    lean_assert_eq(mk_real_type(), Real);
-    env->add_var("i", Int);
-    expr i = Const("i");
-    lean_assert_eq(mk_int_type(), Int);
-}
-
-static void tst1() {
-    environment env;
-    init_test_frontend(env);
-    expr e = mk_int_value(mpz(10));
-    lean_assert(is_int_value(e));
-    lean_assert(type_check(e, env) == Int);
-    std::cout << "e: " << e << "\n";
-}
-
-static void tst2() {
-    environment env;
-    init_test_frontend(env);
-    expr e = mk_Int_add(iVal(10), iVal(30));
-    std::cout << e << "\n";
-    std::cout << normalize(e, env) << "\n";
-    std::cout << type_check(mk_Int_add_fn(), env) << "\n";
-    lean_assert(type_check(e, env) == Int);
-    lean_assert(type_check(mk_app(mk_Int_add_fn(), iVal(10)), env) == (Int >> Int));
-    expr e2 = Fun("a", Int, mk_Int_add(Const("a"), mk_Int_add(iVal(10), iVal(30))));
-    std::cout << e2 << " --> " << normalize(e2, env) << "\n";
-    lean_assert(type_check(e2, env) == mk_arrow(Int, Int));
-}
-
-static void tst3() {
-    environment env;
-    init_test_frontend(env);
-    expr e = mk_Int_mul(iVal(10), iVal(30));
-    std::cout << e << "\n";
-    std::cout << normalize(e, env) << "\n";
-    std::cout << type_check(mk_Int_mul_fn(), env) << "\n";
-    lean_assert(type_check(e, env) == Int);
-    lean_assert(type_check(mk_app(mk_Int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int));
-    expr e2 = Fun("a", Int, mk_Int_mul(Const("a"), mk_Int_mul(iVal(10), iVal(30))));
-    std::cout << e2 << " --> " << normalize(e2, env) << "\n";
-    lean_assert(type_check(e2, env) == (Int >> Int));
-}
-
-static void tst4() {
-    environment env;
-    init_test_frontend(env);
-    expr e = mk_Int_sub(iVal(10), iVal(30));
-    std::cout << e << "\n";
-    std::cout << normalize(e, env) << "\n";
-    std::cout << type_check(mk_Int_sub_fn(), env) << "\n";
-    lean_assert(type_check(e, env) == Int);
-    lean_assert(type_check(mk_app(mk_Int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int));
-    expr e2 = Fun("a", Int, mk_Int_sub(Const("a"), mk_Int_sub(iVal(10), iVal(30))));
-    std::cout << e2 << " --> " << normalize(e2, env) << "\n";
-    lean_assert(type_check(e2, env) == (Int >> Int));
-}
-
-static void tst5() {
-    environment env;
-    init_test_frontend(env);
-    env->add_var(name("a"), Int);
-    expr e = mk_eq(Int, iVal(3), iVal(4));
-    std::cout << e << " --> " << normalize(e, env) << "\n";
-}
-
-static void tst6() {
-    std::cout << "tst6\n";
-    std::cout << mk_Int_add_fn().raw() << "\n";
-    std::cout << mk_Int_add_fn().raw() << "\n";
-
-    #ifndef __APPLE__
-    thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_Int_add_fn().raw() << "\n"; });
-    t1.join();
-    thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_Int_add_fn().raw() << "\n"; });
-    t2.join();
-    #endif
-    std::cout << mk_Int_add_fn().raw() << "\n";
-}
-
-int main() {
-    save_stack_info();
-    register_modules();
-    tst0();
-    tst1();
-    tst2();
-    tst3();
-    tst4();
-    tst5();
-    tst6();
-    return has_violations() ? 1 : 0;
-}