diff --git a/library/standard/data/list/default.lean b/library/standard/data/list/default.lean
new file mode 100644
index 000000000..6db2c909b
--- /dev/null
+++ b/library/standard/data/list/default.lean
@@ -0,0 +1,7 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import data.list.basic
diff --git a/library/standard/data/nat/default.lean b/library/standard/data/nat/default.lean
new file mode 100644
index 000000000..fe3e364f7
--- /dev/null
+++ b/library/standard/data/nat/default.lean
@@ -0,0 +1,7 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import data.nat.nat1
diff --git a/library/standard/data/option.lean b/library/standard/data/option.lean
index de22f2805..f86193dc4 100644
--- a/library/standard/data/option.lean
+++ b/library/standard/data/option.lean
@@ -1,7 +1,9 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.classes.inhabited
 
 inductive option (A : Type) : Type :=
 | none {} : option A
diff --git a/library/standard/data/pair.lean b/library/standard/data/pair.lean
index ce6d2382e..4df1ca07f 100644
--- a/library/standard/data/pair.lean
+++ b/library/standard/data/pair.lean
@@ -1,7 +1,9 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.classes.inhabited
 
 namespace pair
 inductive pair (A : Type) (B : Type) : Type :=
diff --git a/library/standard/data/set.lean b/library/standard/data/set.lean
index 8f2c93d72..aaa0a2f12 100644
--- a/library/standard/data/set.lean
+++ b/library/standard/data/set.lean
@@ -1,7 +1,9 @@
---- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+------------------------------------------------------------------------------------------------------- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad, Leonardo de Moura
-import logic funext bool
+----------------------------------------------------------------------------------------------------
+
+import logic.axioms.funext data.bool
 using eq_proofs bool
 
 namespace set
diff --git a/library/standard/data/sum.lean b/library/standard/data/sum.lean
index f9970af09..41cf77739 100644
--- a/library/standard/data/sum.lean
+++ b/library/standard/data/sum.lean
@@ -1,7 +1,9 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.prop
 
 namespace sum
 inductive sum (A : Type) (B : Type) : Type :=
diff --git a/library/standard/data/unit.lean b/library/standard/data/unit.lean
index e1352e781..90f1f9e50 100644
--- a/library/standard/data/unit.lean
+++ b/library/standard/data/unit.lean
@@ -1,7 +1,10 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic decidable
+----------------------------------------------------------------------------------------------------
+
+import logic.classes.decidable logic.classes.inhabited
 using decidable
 
 namespace unit
diff --git a/library/standard/logic/axioms/classical.lean b/library/standard/logic/axioms/classical.lean
index 09ecb4d1a..509777bf6 100644
--- a/library/standard/logic/axioms/classical.lean
+++ b/library/standard/logic/axioms/classical.lean
@@ -1,7 +1,11 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic cast
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast
+
 using eq_proofs
 
 axiom prop_complete (a : Prop) : a = true ∨ a = false
diff --git a/library/standard/logic/axioms/examples/diaconescu.lean b/library/standard/logic/axioms/examples/diaconescu.lean
index 795e03a98..d48fb2cf8 100644
--- a/library/standard/logic/axioms/examples/diaconescu.lean
+++ b/library/standard/logic/axioms/examples/diaconescu.lean
@@ -1,7 +1,9 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Leonardo de Moura, Jeremy Avigad
-import logic hilbert funext
+-- Author: Leonardo de Moura
+----------------------------------------------------------------------------------------------------
+
+import logic.axioms.hilbert logic.axioms.funext
 using eq_proofs
 
 -- Diaconescu’s theorem
diff --git a/library/standard/logic/axioms/funext.lean b/library/standard/logic/axioms/funext.lean
index c4a1e330a..9b744ce9a 100644
--- a/library/standard/logic/axioms/funext.lean
+++ b/library/standard/logic/axioms/funext.lean
@@ -1,7 +1,10 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic function
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.eq logic.connectives.function
 using function
 
 -- Function extensionality
diff --git a/library/standard/logic/axioms/hilbert.lean b/library/standard/logic/axioms/hilbert.lean
index 303ec089a..457e08f39 100644
--- a/library/standard/logic/axioms/hilbert.lean
+++ b/library/standard/logic/axioms/hilbert.lean
@@ -1,7 +1,9 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.classes.inhabited
 
 variable epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A
 axiom epsilon_ax {A : Type} {P : A → Prop} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P)
diff --git a/library/standard/logic/axioms/piext.lean b/library/standard/logic/axioms/piext.lean
index bbd897a1d..56c17084b 100644
--- a/library/standard/logic/axioms/piext.lean
+++ b/library/standard/logic/axioms/piext.lean
@@ -1,25 +1,32 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic cast
+----------------------------------------------------------------------------------------------------
+
+import logic.classes.inhabited logic.connectives.cast
 
 -- Pi extensionality
-axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} : (Π x, B x) = (Π x, B' x) → B = B'
+axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} :
+  (Π x, B x) = (Π x, B' x) → B = B'
 
-theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) (a : A) : cast H f a == f a :=
+theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x)
+  (a : A) : cast H f a == f a :=
 have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
 have Hb : B = B', from piext H,
 cast_app' Hb f a
 
-theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H : f == f') : f a == f' a :=
+theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
+  (H : f == f') : f a == f' a :=
 have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
 have Hb : B = B', from piext (type_eq H),
 hcongr1' a H Hb
 
-theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type} {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
-               (Hff' : f == f') (Haa' : a == a') : f a == f' a' :=
+theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type}
+    {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
+    (Hff' : f == f') (Haa' : a == a') : f a == f' a' :=
 have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
   take B B' f f' e, hcongr1 a e,
-have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a', from
-  hsubst Haa' H1,
+have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x),
+    f == f' → f a == f' a', from hsubst Haa' H1,
 H2 B B' f f' Hff'
diff --git a/library/standard/logic/axioms/prop_decidable.lean b/library/standard/logic/axioms/prop_decidable.lean
index 5acdf4d3a..b840ba04c 100644
--- a/library/standard/logic/axioms/prop_decidable.lean
+++ b/library/standard/logic/axioms/prop_decidable.lean
@@ -1,7 +1,10 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import classical hilbert decidable
+----------------------------------------------------------------------------------------------------
+
+import logic.axioms.classical logic.axioms.hilbert logic.classes.decidable
 using decidable
 
 -- Excluded middle + Hilbert implies every proposition is decidable
diff --git a/library/standard/standard.lean b/library/standard/standard.lean
index 28cb338bb..88308857b 100644
--- a/library/standard/standard.lean
+++ b/library/standard/standard.lean
@@ -1,4 +1,6 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic tactic num string pair cast
+----------------------------------------------------------------------------------------------------
+
+import logic tools.tactic data.num data.string data.pair logic.connectives.cast
diff --git a/library/standard/struc/binary.lean b/library/standard/struc/binary.lean
index 301cb7db4..13dd59a00 100644
--- a/library/standard/struc/binary.lean
+++ b/library/standard/struc/binary.lean
@@ -1,7 +1,10 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.eq
 using eq_proofs
 
 namespace binary
diff --git a/library/standard/struc/equivalence.lean b/library/standard/struc/equivalence.lean
index 071450d6a..2ec8e8807 100644
--- a/library/standard/struc/equivalence.lean
+++ b/library/standard/struc/equivalence.lean
@@ -1,7 +1,10 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.prop
 
 namespace equivalence
 section
diff --git a/library/standard/struc/wf.lean b/library/standard/struc/wf.lean
index 4a3d213be..e27f1111f 100644
--- a/library/standard/struc/wf.lean
+++ b/library/standard/struc/wf.lean
@@ -1,7 +1,10 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic classical
+----------------------------------------------------------------------------------------------------
+
+import logic.axioms.classical
 
 -- Well-founded relation definition
 -- We are essentially saying that a relation R is well-founded
@@ -28,4 +31,3 @@ by_contradiction (assume N : ¬∀x, P x,
   have s2 : P r,   from iH r s1,
   have s3 : ¬P r,  from and_elim_left Hr,
   absurd s2 s3)
-