diff --git a/library/hott/hott.md b/library/hott/hott.md
index ace0cee26..2f8c21ef6 100644
--- a/library/hott/hott.md
+++ b/library/hott/hott.md
@@ -2,8 +2,8 @@ standard.hott
 =============
 
 A library for Homotopy Type Theory, which avoid the use of prop. Many
-standard types are imported from `standard.data`, but then theorems
-are proved about them using predicate versions of the logical
+standard types are imported from `data`, but then theorems
+are proved about them using predicativee versions of the logical
 operations. For example, we use the path type, products, sums, sigmas,
 and the empty type, rather than equality, and, or, exists, and
 false. These operations take values in Type rather than Prop.
@@ -18,4 +18,4 @@ with HoTT.
 * [equiv](equiv.lean) : equivalence of types
 * [trunc](trunc.lean) : truncatedness of types
 * [funext](funext.lean) : the functional extensionality axiom
-* [inhabited](inhabited.lean) : a predicative version of the inhabited class
+* [fibrant](fibrant.lean) : a class for fibrant types
diff --git a/library/logic/axioms/examples/examples.md b/library/logic/axioms/examples/examples.md
index dbbb827d8..b768dd0d2 100644
--- a/library/logic/axioms/examples/examples.md
+++ b/library/logic/axioms/examples/examples.md
@@ -1,6 +1,4 @@
 logic.axioms.examples
 =====================
 
-Examples involving the axioms.
-
 * [diaconescu](diaconescu.lean) : Diaconescu's theorem
diff --git a/library/logic/classes/classes.md b/library/logic/classes/classes.md
index 40eaffe00..8a791ab52 100644
--- a/library/logic/classes/classes.md
+++ b/library/logic/classes/classes.md
@@ -6,10 +6,9 @@ Useful classes for general logical manipulations.
 * [inhabited](inhabited.lean) : inhabited types
 * [nonempty](nonempty.lean) : nonempty type
 * [decidable](decidable.lean) : decidable types
-* [congr](congr.lean) : congruences with respect to suitable relations
 
 Constructively, inhabited types have a witness, while nonempty types
-are "proof irrelevant". Classically (assuming the axiom in
+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
diff --git a/library/logic/default.lean b/library/logic/default.lean
index 0040821d8..b71c7a420 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -1,9 +1,9 @@
-----------------------------------------------------------------------------------------------------
 --- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
-----------------------------------------------------------------------------------------------------
 
-import logic.connectives.basic logic.connectives.eq logic.connectives.quantifiers
-import logic.classes.decidable logic.classes.inhabited logic.connectives.instances
-import logic.connectives.if logic.connectives.identities
\ No newline at end of file
+import logic.connectives.basic logic.connectives.eq logic.connectives.cast 
+import logic.connectives.quantifiers logic.connectives.if 
+import logic.classes.decidable logic.classes.inhabited logic.classes.nonempty
+import logic.connectives.instances
+import logic.connectives.identities
\ No newline at end of file
diff --git a/library/logic/logic.md b/library/logic/logic.md
index 8638073d3..9386ca6bb 100644
--- a/library/logic/logic.md
+++ b/library/logic/logic.md
@@ -1,9 +1,11 @@
 logic
 =====
 
-Logical constructions and axioms. By default, `import logic` does not import any additional axioms.
+Logical constructions and axioms. By default, `import logic` does not
+import any additional axioms.
 
 * [connectives](connectives/connectives.md) : logical connectives
 * [axioms](axioms/axioms.md) : additional axioms
-* [classes](classes/classes.md) : classes for inhabited types, decidable types, etc.
+* [classes](classes/classes.md) : classes for inhabited types, 
+decidable types, etc.  
 * [examples](examples/examples.md)
\ No newline at end of file
diff --git a/library/standard.lean b/library/standard.lean
index 98096a5c3..692eaa9fc 100644
--- a/library/standard.lean
+++ b/library/standard.lean
@@ -2,4 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic tools.tactic data.num data.string data.prod logic.connectives.cast
+-- changing to this breaks some tests:
+-- import logic data tools.tactic
+
+import logic tools.tactic data.num data.string data.prod logic.connectives.cast
\ No newline at end of file
diff --git a/library/standard.md b/library/standard.md
index b0c6e03ed..c0f4b3848 100644
--- a/library/standard.md
+++ b/library/standard.md
@@ -2,11 +2,11 @@ standard
 ========
 
 The Lean standard library. By default, `import standard` does not
-import the classical axioms. For that, use `import logic.axioms`.
+import any axioms. See logic.axioms.
 
 * [general_notation](general_notation.lean) : notation shared by all libraries
 * [logic](logic/logic.md) : logical constructs and axioms
 * [data](data/data.md) : various datatypes
 * [struc](struc/struc.md) : axiomatic structures
 * [hott](hott/hott.md) : homotopy type theory
-* [tools](tools/tool.md) : various additional tools
\ No newline at end of file
+* [tools](tools/tools.md) : various additional tools
\ No newline at end of file