diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
index fa7256912..d951bd2f0 100644
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@@ -48,8 +48,8 @@ let u : {x | (∃y, P y) → P x} :=
 has_property u Hex
 
 theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
-    P (@epsilon A (exists_imp_nonempty Hex) P) :=
-epsilon_spec_aux (exists_imp_nonempty Hex) P Hex
+    P (@epsilon A (nonempty_of_exists Hex) P) :=
+epsilon_spec_aux (nonempty_of_exists Hex) P Hex
 
 theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a :=
 epsilon_spec (exists_intro a (eq.refl a))
@@ -60,7 +60,7 @@ epsilon_spec (exists_intro a (eq.refl a))
 
 theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) :
   ∃f, ∀x, R x (f x) :=
-let f := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y),
+let f := λx, @epsilon _ (nonempty_of_exists (H x)) (λy, R x y),
     H := take x, epsilon_spec (H x)
 in exists_intro f H
 
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index 396ef4c63..6291b7bb8 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -1,12 +1,16 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: cast.lean
+Author: Leonardo de Moura
+
+Casts and heterogeneous equality. See also init.datatypes and init.logic.
+-/
+
 import logic.eq logic.quantifiers
 open eq.ops
 
--- cast.lean
--- =========
-
 section
   universe variable u
   variables {A B : Type.{u}}
@@ -30,20 +34,24 @@ namespace heq
   definition type_eq (H : a == b) : A = B :=
   heq.rec_on H (eq.refl A)
 
-  theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
+  theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) :
+    C b H₁ :=
   rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
 
   theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b :=
   drec_on H !cast_eq
 end heq
 
-theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p :=
+theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) :
+  eq.rec_on H p == p :=
 eq.drec_on H !heq.refl
 
 section
   universe variables u v
   variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}
-  theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') : f a == f' a :=
+
+  theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') :
+    f a == f' a :=
   have aux : ∀ (f : Π x, P x) (f' : Π x, P x), f == f' → f a == f' a, from
     take f f' H, heq.to_eq H ▸ heq.refl (f a),
   (H₂ ▸ aux) f f' H₁
@@ -105,10 +113,11 @@ section
     take H : P = P, heq.refl (eq.rec_on H f a),
   (H ▸ aux) H
 
-  theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
+  theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) :
+    eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
   heq.to_eq (calc
-    eq.rec_on H f a == f a                             : rec_on_app H f a
-              ...   == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
+    eq.rec_on H f a == f a                   : rec_on_app H f a
+      ... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
 
   theorem cast_app (H : P = P') (f : Π x, P x) (a : A) : cast (pi_eq H) f a == f a :=
   have H₁ : ∀ (H : (Π x, P x) = (Π x, P x)), cast H f a == f a, from
@@ -116,7 +125,6 @@ section
   have H₂ : ∀ (H : (Π x, P x) = (Π x, P' x)), cast H f a == f a, from
     H ▸ H₁,
   H₂ (pi_eq H)
-
 end
 
 section
@@ -144,7 +152,8 @@ section
       (Hd : cast (dcongr_arg3 D Ha Hb Hc) d = d') : f a b c d = f a' b' c' d' :=
   heq.to_eq (hcongr_arg4 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
 
-  --mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition. Then proving eq is easier than proving heq)
+  -- mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition.
+  -- Then proving eq is easier than proving heq)
   theorem hdcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : b == b')
       (Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c')
         : f a b c = f a' b' c' :=
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index f8516abf8..c7b302424 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: logic.connectives
 Authors: Jeremy Avigad, Leonardo de Moura
 
-The propositional connectives. See also init.datatypes.
+The propositional connectives. See also init.datatypes and init.logic.
 -/
 
 variables {a b c d : Prop}
diff --git a/library/logic/default.lean b/library/logic/default.lean
index 4d5618f4f..246901e26 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -1,6 +1,10 @@
---- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
---- Released under Apache 2.0 license as described in the file LICENSE.
---- Author: Jeremy Avigad
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: logic.default
+Author: Jeremy Avigad
+-/
 
 import logic.eq logic.connectives logic.cast logic.subsingleton
 import logic.quantifiers logic.instances logic.identities
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index db7387743..ecb57f87a 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -1,16 +1,13 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: logic.eq
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 
-Additional declarations/theorems about equality
+Additional declarations/theorems about equality. See also init.datatypes and init.logic.
 -/
 
--- logic.eq
--- ========
-
--- Equality.
-
 open eq.ops
 
 namespace eq
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index 3aaa98477..6e4f50a0c 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -1,36 +1,37 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Jeremy Avigad, Leonardo de Moura
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 
--- logic.identities
--- ============================
+Module: logic.identities
+Authors: Jeremy Avigad, Leonardo de Moura
 
--- Useful logical identities. In the absence of propositional extensionality, some of the
--- calculations use the type class support provided by logic.instances
+Useful logical identities. Since we are not using propositional extensionality, some of the
+calculations use the type class support provided by logic.instances.
+-/
 
 import logic.connectives logic.instances logic.quantifiers logic.cast
 
 open relation decidable relation.iff_ops
 
-theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
+theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
 calc
   (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or.assoc
     ... ↔ a ∨ (c ∨ b)       : {or.comm}
      ... ↔ (a ∨ c) ∨ b      : iff.symm or.assoc
 
-theorem or_left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) :=
+theorem or.left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) :=
 calc
   a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc
     ... ↔ (b ∨ a) ∨ c       : {or.comm}
      ... ↔ b ∨ (a ∨ c)      : or.assoc
 
-theorem and_right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
+theorem and.right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
 calc
   (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc
     ... ↔ a ∧ (c ∧ b)       : {and.comm}
      ... ↔ (a ∧ c) ∧ b      : iff.symm and.assoc
 
-theorem and_left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) :=
+theorem and.left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) :=
 calc
   a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc
     ... ↔ (b ∧ a) ∧ c       : {and.comm}
@@ -46,14 +47,14 @@ iff.intro
 theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a :=
 iff.mp not_not_iff H
 
-theorem not_true_iff_false : (¬true) ↔ false :=
+theorem not_true_iff_false : ¬true ↔ false :=
 iff.intro (assume H, H trivial) false.elim
 
-theorem not_false_iff_true : (¬false) ↔ true :=
+theorem not_false_iff_true : ¬false ↔ true :=
 iff.intro (assume H, trivial) (assume H H', H')
 
 theorem not_or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
-  (¬(a ∨ b)) ↔ (¬a ∧ ¬b) :=
+  ¬(a ∨ b) ↔ ¬a ∧ ¬b :=
 iff.intro
   (assume H, or.elim (em a)
     (assume Ha, absurd (or.inl Ha) H)
@@ -65,7 +66,8 @@ iff.intro
       (assume Ha, absurd Ha (and.elim_left H))
       (assume Hb, absurd Hb (and.elim_right H)))
 
-theorem not_and {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) :=
+theorem not_and_iff_not_or_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
+  ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
 iff.intro
   (assume H, or.elim (em a)
     (assume Ha, or.elim (em b)
@@ -77,7 +79,7 @@ iff.intro
       (assume Hna, absurd (and.elim_left N) Hna)
       (assume Hnb, absurd (and.elim_right N) Hnb))
 
-theorem imp_or {a b : Prop} [Da : decidable a] : (a → b) ↔ (¬a ∨ b) :=
+theorem imp_iff_not_or {a b : Prop} [Da : decidable a] : (a → b) ↔ ¬a ∨ b :=
 iff.intro
   (assume H : a → b, (or.elim (em a)
     (assume Ha  : a,   or.inr (H Ha))
@@ -85,27 +87,29 @@ iff.intro
   (assume (H : ¬a ∨ b) (Ha : a),
     or_resolve_right H (not_not_iff⁻¹ ▸ Ha))
 
-theorem not_implies {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a → b)) ↔ (a ∧ ¬b) :=
-calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or}
-            ... ↔ (¬¬a ∧ ¬b)  : not_or_iff_not_and_not
-            ... ↔ (a ∧ ¬b)    : {not_not_iff}
+theorem not_implies_iff_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
+  ¬(a → b) ↔ a ∧ ¬b :=
+calc
+  ¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or}
+       ... ↔ ¬¬a ∧ ¬b  : not_or_iff_not_and_not
+       ... ↔ a ∧ ¬b    : {not_not_iff}
 
 theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a :=
 assume H, by_contradiction (assume Hna : ¬a,
   have Hnna : ¬¬a, from not_not_of_not_implies (mt H Hna),
   absurd (not_not_elim Hnna) Hna)
 
-theorem not_exists_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
+theorem forall_not_of_not_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
     (H : ¬∃x, P x) : ∀x, ¬P x :=
 take x, or.elim (em (P x))
   (assume Hp : P x,   absurd (exists_intro x Hp) H)
   (assume Hn : ¬P x, Hn)
 
-theorem not_forall_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
+theorem exists_not_of_not_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
     [D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) :
   ∃x, ¬P x :=
 @by_contradiction _ D' (assume H1 : ¬∃x, ¬P x,
-  have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not.decidable (D x)) H1,
+  have H2 : ∀x, ¬¬P x, from @forall_not_of_not_exists _ _ (take x, not.decidable (D x)) H1,
   have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x),
   absurd H3 H)
 
@@ -119,32 +123,32 @@ iff.intro
   (assume H1 : a,     absurd H1 H)
   (assume H2 : false, false.elim H2)
 
-theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false :=
+theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false :=
 iff.intro
   (assume H, false.of_ne H)
   (assume H, false.elim H)
 
-theorem eq_id {A : Type} (a : A) : (a = a) ↔ true :=
+theorem eq_self_iff_true {A : Type} (a : A) : (a = a) ↔ true :=
 iff_true_intro rfl
 
-theorem heq_id {A : Type} (a : A) : (a == a) ↔ true :=
+theorem heq_self_iff_true {A : Type} (a : A) : (a == a) ↔ true :=
 iff_true_intro (heq.refl a)
 
-theorem a_iff_not_a (a : Prop) : (a ↔ ¬a) ↔ false :=
+theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
 iff.intro
   (assume H,
     have H' : ¬a, from assume Ha, (H ▸ Ha) Ha,
     H' (H⁻¹ ▸ H'))
   (assume H, false.elim H)
 
-theorem true_eq_false : (true ↔ false) ↔ false :=
-not_true_iff_false ▸ (a_iff_not_a true)
+theorem true_iff_false : (true ↔ false) ↔ false :=
+not_true_iff_false ▸ (iff_not_self true)
 
-theorem false_eq_true : (false ↔ true) ↔ false :=
-not_false_iff_true ▸ (a_iff_not_a false)
+theorem false_iff_true : (false ↔ true) ↔ false :=
+not_false_iff_true ▸ (iff_not_self false)
 
-theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a :=
+theorem iff_true_iff (a : Prop) : (a ↔ true) ↔ a :=
 iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H)
 
-theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a :=
+theorem iff_false_iff_not (a : Prop) : (a ↔ false) ↔ ¬a :=
 iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H)
diff --git a/library/logic/instances.lean b/library/logic/instances.lean
index 4b0853a8d..f5da26e7a 100644
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@@ -20,7 +20,6 @@ relation.is_equivalence.mk (@eq.refl T) (@eq.symm T) (@eq.trans T)
 theorem is_equivalence_iff [instance] : relation.is_equivalence iff :=
 relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans
 
-
 /- congruences for logic operations -/
 
 theorem is_congruence_not : is_congruence iff iff not :=
@@ -62,14 +61,12 @@ is_congruence2.mk
       (assume H3 : a1 ↔ a2, iff.trans (iff.symm H1) (iff.trans H3 H2))
       (assume H3 : b1 ↔ b2, iff.trans H1 (iff.trans H3 (iff.symm H2))))
 
--- theorem is_congruence_const_iff [instance] := is_congruence.const iff iff.refl
 definition is_congruence_not_compose [instance] := is_congruence.compose is_congruence_not
 definition is_congruence_and_compose [instance] := is_congruence.compose21 is_congruence_and
 definition is_congruence_or_compose [instance] := is_congruence.compose21 is_congruence_or
 definition is_congruence_implies_compose [instance] := is_congruence.compose21 is_congruence_imp
 definition is_congruence_iff_compose [instance] := is_congruence.compose21 is_congruence_iff
 
-
 /- a general substitution operation with respect to an arbitrary congruence -/
 
 namespace general_subst
@@ -77,13 +74,11 @@ namespace general_subst
     {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (is_congruence.app C H) H1
 end general_subst
 
-
 /- iff can be coerced to implication -/
 
 definition mp_like_iff [instance] : relation.mp_like iff :=
 relation.mp_like.mk (λa b (H : a ↔ b), iff.elim_left H)
 
-
 /- support for calculations with iff -/
 
 namespace iff
diff --git a/library/logic/logic.md b/library/logic/logic.md
index c86ef3c66..2a97b5dd8 100644
--- a/library/logic/logic.md
+++ b/library/logic/logic.md
@@ -1,22 +1,22 @@
 logic
 =====
 
-Additional constructions and axioms. By default, `import logic` does not
-import any axioms.
+Logical constructions and theorems, beyond what has already been
+declared in init.datatypes and init.logic. 
 
-Logical operations and connectives.
+The subfolder logic.axioms declares additional axioms. The command
+`import logic` does not import any axioms by default.
 
+* [connectives](connectives.lean) : the propositional connectives
 * [eq](eq.lean) : additional theorems for equality and disequality
 * [cast](cast.lean) : casts and heterogeneous equality
 * [quantifiers](quantifiers.lean) : existential and universal quantifiers
 * [identities](identities.lean) : some useful identities
+* [instances](instances.lean) : class instances for eq and iff
+* [subsingleton](subsingleton.lean)
+* [default](default.lean)
 
-Constructively, inhabited types have a witness, while nonempty types
-are "proof irrelevant". Classically (assuming the axioms in
-logic.axioms.hilbert) the two are equivalent. Type class inferences
-are set up to use "inhabited" however, so users should use that to
-declare that types have an element. Use "nonempty" in the hypothesis
-of a theorem when the theorem does not depend on the witness chosen.
+Subfolders:
 
 * [axioms](axioms/axioms.md) : additional axioms
 * [examples](examples/examples.md)
\ No newline at end of file
diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean
index 7b01e7ed6..67847ca4a 100644
--- a/library/logic/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@@ -4,16 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: logic.quantifiers
 Authors: Leonardo de Moura, Jeremy Avigad
+
+Universal and existential quantifiers. See also init.logic.
 -/
 
 open inhabited nonempty
 
-theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
+theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
 assume H1 : ∀x, ¬p x,
   obtain (w : A) (Hw : p w), from H,
   absurd Hw (H1 w)
 
-theorem forall_not_exists {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
+theorem not_exists_not_of_forall {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
 assume H1 : ∃x, ¬p x,
   obtain (w : A) (Hw : ¬p w), from H1,
   absurd (H2 w) Hw
@@ -41,12 +43,14 @@ iff.intro
   (assume Hl, obtain a Hp, from Hl, Hp)
   (assume Hr, inhabited.destruct H (take a, exists_intro a Hr))
 
-theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
+theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) :
+  (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
 iff.intro
   (assume H, and.intro (take x, and.elim_left (H x)) (take x, and.elim_right (H x)))
   (assume H, take x, and.intro (and.elim_left H x) (and.elim_right H x))
 
-theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) :=
+theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) :
+  (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) :=
 iff.intro
   (assume H, obtain (w : A) (Hw : φ w ∨ ψ w), from H,
     or.elim Hw
@@ -58,7 +62,7 @@ iff.intro
     (assume H2, obtain (w : A) (Hw : ψ w), from H2,
       exists_intro w (or.inr Hw)))
 
-theorem exists_imp_nonempty {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A :=
+theorem nonempty_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A :=
 obtain w Hw, from H, nonempty.intro w
 
 section
diff --git a/library/logic/subsingleton.lean b/library/logic/subsingleton.lean
index 2efb27125..0fe2e0ddc 100644
--- a/library/logic/subsingleton.lean
+++ b/library/logic/subsingleton.lean
@@ -1,8 +1,11 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
+
+Module: logic.subsingleton
+Author: Floris van Doorn
 -/
+
 import logic.eq
 
 inductive subsingleton [class] (A : Type) : Prop :=
@@ -28,7 +31,8 @@ subsingleton.intro (fun d1 d2,
       d2)
    d1)
 
-protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
+protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p]
+    {H1 : p → Type} {H2 : ¬p → Type}
     (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
-    : subsingleton (decidable.rec_on H H1 H2) :=
+  : subsingleton (decidable.rec_on H H1 H2) :=
 decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"