diff --git a/library/init/classical.lean b/library/init/classical.lean
deleted file mode 100644
index ad6700409f..0000000000
--- a/library/init/classical.lean
+++ /dev/null
@@ -1,167 +0,0 @@
-/-
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
--/
-prelude
-import init.core
-
-namespace classical
-universes u v
-
-/- the axiom -/
-axiom choice {α : Sort u} : nonempty α → α
-
-noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop)
-  (h : ∃ x, p x) : {x // p x} :=
-choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩
-
-noncomputable def some {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
-(indefinite_description p h).val
-
-theorem some_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (some h) :=
-(indefinite_description p h).property
-
-/- Diaconescu's theorem: using function extensionality and propositional extensionality,
-   we can get excluded middle from this. -/
-section diaconescu
-parameter  p : Prop
-
-private def U (x : Prop) : Prop := x = true ∨ p
-private def V (x : Prop) : Prop := x = false ∨ p
-
-private lemma exU : ∃ x, U x := ⟨true, or.inl rfl⟩
-private lemma exV : ∃ x, V x := ⟨false, or.inl rfl⟩
-
-/- TODO(Leo): check why the code generator is not ignoring (some exU)
-   when we mark u as def. -/
-private lemma u : Prop := some exU
-private lemma v : Prop := some exV
-
-set_option type_context.unfold_lemmas true
-private lemma u_def : U u := some_spec exU
-private lemma v_def : V v := some_spec exV
-
-private lemma not_uv_or_p : u ≠ v ∨ p :=
-or.elim u_def
-  (assume hut : u = true,
-    or.elim v_def
-      (assume hvf : v = false,
-        have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ true_ne_false,
-        or.inl hne)
-      or.inr)
-  or.inr
-
-private lemma p_implies_uv (hp : p) : u = v :=
-have hpred : U = V, from
-  funext (assume x : Prop,
-    have hl : (x = true ∨ p) → (x = false ∨ p), from
-      assume a, or.inr hp,
-    have hr : (x = false ∨ p) → (x = true ∨ p), from
-      assume a, or.inr hp,
-    show (x = true ∨ p) = (x = false ∨ p), from
-      propext (iff.intro hl hr)),
-have h₀ : ∀ exU exV,
-    @some _ U exU = @some _ V exV,
-  from hpred ▸ λ exU exV, rfl,
-show u = v, from h₀ _ _
-
-theorem em : p ∨ ¬p :=
-or.elim not_uv_or_p
-  (assume hne : u ≠ v, or.inr (mt p_implies_uv hne))
-  or.inl
-end diaconescu
-
-theorem exists_true_of_nonempty {α : Sort u} : nonempty α → ∃ x : α, true
-| ⟨x⟩ := ⟨x, trivial⟩
-
-noncomputable def inhabited_of_nonempty {α : Sort u} (h : nonempty α) : inhabited α :=
-⟨choice h⟩
-
-noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :
-  inhabited α :=
-inhabited_of_nonempty (exists.elim h (λ w hw, ⟨w⟩))
-
-/- all propositions are decidable -/
-noncomputable def prop_decidable (a : Prop) : decidable a :=
-choice $ or.elim (em a)
-  (assume ha, ⟨is_true ha⟩)
-  (assume hna, ⟨is_false hna⟩)
-local attribute [instance] prop_decidable
-
-noncomputable def decidable_inhabited (a : Prop) : inhabited (decidable a) :=
-⟨prop_decidable a⟩
-local attribute [instance] decidable_inhabited
-
-noncomputable def type_decidable_eq (α : Sort u) : decidable_eq α :=
-λ x y, prop_decidable (x = y)
-
-noncomputable def type_decidable (α : Sort u) : psum α (α → false) :=
-match (prop_decidable (nonempty α)) with
-| (is_true hp)  := psum.inl (@inhabited.default _ (inhabited_of_nonempty hp))
-| (is_false hn) := psum.inr (λ a, absurd (nonempty.intro a) hn)
-end
-
-noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Prop)
-  (h : nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
-if hp : ∃ x : α, p x then
-  let xp := indefinite_description _ hp in
-  ⟨xp.val, λ h', xp.property⟩
-else ⟨choice h, λ h, absurd h hp⟩
-
-/- the Hilbert epsilon function -/
-
-noncomputable def epsilon {α : Sort u} [h : nonempty α] (p : α → Prop) : α :=
-(strong_indefinite_description p h).val
-
-theorem epsilon_spec_aux {α : Sort u} (h : nonempty α) (p : α → Prop)
-  : (∃ y, p y) → p (@epsilon α h p) :=
-(strong_indefinite_description p h).property
-
-theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) :
-    p (@epsilon α (nonempty_of_exists hex) p) :=
-epsilon_spec_aux (nonempty_of_exists hex) p hex
-
-theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y = x) = x :=
-@epsilon_spec α (λ y, y = x) ⟨x, rfl⟩
-
-/- the axiom of choice -/
-
-theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
-  ∃ (f : Π x, β x), ∀ x, r x (f x) :=
-⟨_, λ x, some_spec (h x)⟩
-
-theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
-  (∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, b x), ∀ x, p x (f x) :=
-⟨axiom_of_choice, λ ⟨f, hw⟩ x, ⟨f x, hw x⟩⟩
-
-theorem prop_complete (a : Prop) : a = true ∨ a = false :=
-or.elim (em a)
-  (λ t, or.inl (eq_true_intro t))
-  (λ f, or.inr (eq_false_intro f))
-
-def eq_true_or_eq_false := prop_complete
-
-section aux
-attribute [elab_as_eliminator]
-theorem cases_true_false (p : Prop → Prop) (h1 : p true) (h2 : p false) (a : Prop) : p a :=
-or.elim (prop_complete a)
-  (assume ht : a = true,  ht.symm ▸ h1)
-  (assume hf : a = false, hf.symm ▸ h2)
-
-theorem cases_on (a : Prop) {p : Prop → Prop} (h1 : p true) (h2 : p false) : p a :=
-cases_true_false p h1 h2 a
-
--- this supercedes by_cases in decidable
-def by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
-decidable.by_cases hpq hnpq
-
--- this supercedes by_contradiction in decidable
-theorem by_contradiction {p : Prop} (h : ¬p → false) : p :=
-decidable.by_contradiction h
-
-theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
-(prop_complete a).symm
-end aux
-
-end classical
diff --git a/library/init/core.lean b/library/init/core.lean
index ca52d94d34..79e989c94a 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -2096,3 +2096,161 @@ local infix `~` := function.equiv
 
 instance pi.subsingleton {α : Sort u} {β : α → Sort v} [∀ a, subsingleton (β a)] : subsingleton (Π a, β a) :=
 ⟨λ f₁ f₂, funext (λ a, subsingleton.elim (f₁ a) (f₂ a))⟩
+
+/- Classical reasoning support -/
+
+namespace classical
+
+axiom choice {α : Sort u} : nonempty α → α
+
+noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop)
+  (h : ∃ x, p x) : {x // p x} :=
+choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩
+
+noncomputable def some {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
+(indefinite_description p h).val
+
+theorem some_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (some h) :=
+(indefinite_description p h).property
+
+/- Diaconescu's theorem: using function extensionality and propositional extensionality,
+   we can get excluded middle from this. -/
+section diaconescu
+parameter  p : Prop
+
+private def U (x : Prop) : Prop := x = true ∨ p
+private def V (x : Prop) : Prop := x = false ∨ p
+
+private theorem exU : ∃ x, U x := ⟨true, or.inl rfl⟩
+private theorem exV : ∃ x, V x := ⟨false, or.inl rfl⟩
+
+private theorem u : Prop := some exU
+private theorem v : Prop := some exV
+
+set_option type_context.unfold_lemmas true
+private theorem u_def : U u := some_spec exU
+private theorem v_def : V v := some_spec exV
+
+private theorem not_uv_or_p : u ≠ v ∨ p :=
+or.elim u_def
+  (assume hut : u = true,
+    or.elim v_def
+      (assume hvf : v = false,
+        have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ true_ne_false,
+        or.inl hne)
+      or.inr)
+  or.inr
+
+private theorem p_implies_uv (hp : p) : u = v :=
+have hpred : U = V, from
+  funext (assume x : Prop,
+    have hl : (x = true ∨ p) → (x = false ∨ p), from
+      assume a, or.inr hp,
+    have hr : (x = false ∨ p) → (x = true ∨ p), from
+      assume a, or.inr hp,
+    show (x = true ∨ p) = (x = false ∨ p), from
+      propext (iff.intro hl hr)),
+have h₀ : ∀ exU exV,
+    @some _ U exU = @some _ V exV,
+  from hpred ▸ λ exU exV, rfl,
+show u = v, from h₀ _ _
+
+theorem em : p ∨ ¬p :=
+or.elim not_uv_or_p
+  (assume hne : u ≠ v, or.inr (mt p_implies_uv hne))
+  or.inl
+end diaconescu
+
+theorem exists_true_of_nonempty {α : Sort u} : nonempty α → ∃ x : α, true
+| ⟨x⟩ := ⟨x, trivial⟩
+
+noncomputable def inhabited_of_nonempty {α : Sort u} (h : nonempty α) : inhabited α :=
+⟨choice h⟩
+
+noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :
+  inhabited α :=
+inhabited_of_nonempty (exists.elim h (λ w hw, ⟨w⟩))
+
+/- all propositions are decidable -/
+noncomputable def prop_decidable (a : Prop) : decidable a :=
+choice $ or.elim (em a)
+  (assume ha, ⟨is_true ha⟩)
+  (assume hna, ⟨is_false hna⟩)
+local attribute [instance] prop_decidable
+
+noncomputable def decidable_inhabited (a : Prop) : inhabited (decidable a) :=
+⟨prop_decidable a⟩
+local attribute [instance] decidable_inhabited
+
+noncomputable def type_decidable_eq (α : Sort u) : decidable_eq α :=
+λ x y, prop_decidable (x = y)
+
+noncomputable def type_decidable (α : Sort u) : psum α (α → false) :=
+match (prop_decidable (nonempty α)) with
+| (is_true hp)  := psum.inl (@inhabited.default _ (inhabited_of_nonempty hp))
+| (is_false hn) := psum.inr (λ a, absurd (nonempty.intro a) hn)
+end
+
+noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Prop)
+  (h : nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
+if hp : ∃ x : α, p x then
+  let xp := indefinite_description _ hp in
+  ⟨xp.val, λ h', xp.property⟩
+else ⟨choice h, λ h, absurd h hp⟩
+
+/- the Hilbert epsilon function -/
+
+noncomputable def epsilon {α : Sort u} [h : nonempty α] (p : α → Prop) : α :=
+(strong_indefinite_description p h).val
+
+theorem epsilon_spec_aux {α : Sort u} (h : nonempty α) (p : α → Prop)
+  : (∃ y, p y) → p (@epsilon α h p) :=
+(strong_indefinite_description p h).property
+
+theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) :
+    p (@epsilon α (nonempty_of_exists hex) p) :=
+epsilon_spec_aux (nonempty_of_exists hex) p hex
+
+theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y = x) = x :=
+@epsilon_spec α (λ y, y = x) ⟨x, rfl⟩
+
+/- the axiom of choice -/
+
+theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
+  ∃ (f : Π x, β x), ∀ x, r x (f x) :=
+⟨_, λ x, some_spec (h x)⟩
+
+theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
+  (∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, b x), ∀ x, p x (f x) :=
+⟨axiom_of_choice, λ ⟨f, hw⟩ x, ⟨f x, hw x⟩⟩
+
+theorem prop_complete (a : Prop) : a = true ∨ a = false :=
+or.elim (em a)
+  (λ t, or.inl (eq_true_intro t))
+  (λ f, or.inr (eq_false_intro f))
+
+def eq_true_or_eq_false := prop_complete
+
+section aux
+attribute [elab_as_eliminator]
+theorem cases_true_false (p : Prop → Prop) (h1 : p true) (h2 : p false) (a : Prop) : p a :=
+or.elim (prop_complete a)
+  (assume ht : a = true,  ht.symm ▸ h1)
+  (assume hf : a = false, hf.symm ▸ h2)
+
+theorem cases_on (a : Prop) {p : Prop → Prop} (h1 : p true) (h2 : p false) : p a :=
+cases_true_false p h1 h2 a
+
+-- this supercedes by_cases in decidable
+def by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
+decidable.by_cases hpq hnpq
+
+-- this supercedes by_contradiction in decidable
+theorem by_contradiction {p : Prop} (h : ¬p → false) : p :=
+decidable.by_contradiction h
+
+theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
+(prop_complete a).symm
+end aux
+
+end classical
diff --git a/library/init/default.lean b/library/init/default.lean
index 5fa99018fe..15c0ce3c53 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.core init.control init.data.basic init.version
-import init.function init.classical
-import init.util init.coe init.wf init.meta init.meta.well_founded_tactics init.data
+import init.function init.util init.coe init.wf init.meta
+import init.meta.well_founded_tactics init.data
 
 @[user_attribute]
 meta def debugger.attr : user_attribute :=